review

Author: Tragicus

HB/structure.elpi

@@ -296,19 +296,21 @@ mk-sort-coercion-aux _ Structure P Args Clause :-
   std.rev Args ArgsRev,
   Clause =
     (pi ctx v t e r argsAll w\ (coercion ctx v (app [Structure | ArgsRev]) e r :-
+		coq.say "try sort coercion",
       std.append ArgsRev [v] argsAll,
       coq.mk-app P argsAll w,
+		coq.say "find coercion from sort",
       coq.elaborate-skeleton w e r ok,
-      coq.ltac.collect-goals r [] [])).
+      coq.ltac.collect-goals r [] [],
+		coq.say "sort coercion succeeds")).
 
 pred mk-sort-coercion i:term, i:term, o:prop.
 mk-sort-coercion Structure P Clause :-
-  coq.typecheck Structure T ok,
+  std.assert-ok! (coq.typecheck Structure T) "anomaly: mk-sort-coercion",
   mk-sort-coercion-aux T Structure P [] Clause.
 
 pred mk-reverse-coercion-aux i:term, i:term, i:term, i:list term, o:prop.
-mk-reverse-coercion-aux (prod _N _T Body) Structure G Args Clause :-
-  Clause = (pi x\ C x),
+mk-reverse-coercion-aux (prod _N _T Body) Structure G Args (pi x\ C x) :-
   pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).
 
 mk-reverse-coercion-aux _ Structure G Args Clause :-
@@ -322,7 +324,7 @@ mk-reverse-coercion-aux _ Structure G Args Clause :-
 
 pred mk-reverse-coercion i:gref, o:prop.
 mk-reverse-coercion Structure Clause :-
-  coq.typecheck (global Structure) T ok,
+  coq.env.typeof Structure T,
   get-constructor Structure G,
   mk-reverse-coercion-aux T (global Structure) (global G) [] Clause.
 

structures.v

@@ -15,7 +15,8 @@ Definition ignore {T} (x: T) := x.
 Definition ignore_disabled {T T'} (x : T) (x' : T') := x'.
 
 (* ********************* structures ****************************** *)
-From elpi Require Import elpi coercion.
+From elpi Require Import elpi.
+From elpi.apps Require Import coercion.
 
 Register unify as hb.unify.
 Register id_phant as hb.id.