updated for the new version of mathQL.ml

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 42ee2c1609b9ab6d18a0f8bf30326c5cd326d930..c605d41a97d2848eca8fd05c4575d8e8aa46d184 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -133,7 +133,6 @@ let metas_in_term term =
     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
     | C.Const _
-    | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ -> []
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -450,7 +449,6 @@ let eta_expand metasenv context t arg =
     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
     | C.Appl l -> C.Appl (List.map (aux n) l)
     | C.Const _ as t -> t
-    | C.Abst _ -> assert false
     | C.MutInd _
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -579,6 +577,7 @@ let elim_intros_simpl term =
                  | _ ->raise NotTheRightEliminatorShape
                in
                 find_head he,fargs
+            | C.Meta (emeta,_) -> emeta,[]
 (* *)
             | _ -> raise NotTheRightEliminatorShape
           in
@@ -749,8 +748,10 @@ let fold term =
    (* the type of one metavariable. So we replace it everywhere.   *)
    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
-   let replace = ProofEngineReduction.replace
-    ~equality:(==) ~what:term' ~with_what:term
+   let replace =
+    ProofEngineReduction.replace
+     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~what:term' ~with_what:term
    in
     let ty' = replace ty in
     let context' =