first moogle template checkin

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index c70be1fb736b61b4da38d15c491f2e5d77579f18..99eb43f6a56e65e8419b090e43a0d2016dd6651b 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -142,7 +142,7 @@ let replace ~equality ~what ~with_what ~where =
         C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
      | C.Meta _ -> t
      | C.Sort _ -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
@@ -216,7 +216,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
     | C.Prod (n,s,t) ->
        C.Prod
@@ -315,7 +315,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
         in
          C.Meta(i,l')
      | C.Sort _ as t -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
      | C.Prod (n,s,t) ->
         C.Prod (n, substaux k s, substaux (k + 1) t)
@@ -382,7 +382,7 @@ let reduce context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
+         | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
         | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) ->
@@ -402,7 +402,7 @@ let reduce context =
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) ->
        C.Cast (reduceaux context l te, reduceaux context l ty)
     | C.Prod (name,s,t) ->
@@ -506,7 +506,7 @@ let reduce context =
                 eat_first (r,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit _ ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in
@@ -604,7 +604,7 @@ let simpl context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def bo) ->
+         | Some (_,C.Def (bo,_)) ->
             try_delta_expansion l t (S.lift n bo)
         | None -> raise RelToHiddenHypothesis
        )
@@ -625,7 +625,7 @@ let simpl context =
         )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) ->
        C.Cast (reduceaux context l te, reduceaux context l ty)
     | C.Prod (name,s,t) ->
@@ -726,7 +726,7 @@ let simpl context =
                 eat_first (r,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit _ ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in