changed proofStatus so that uri component is optional (useful to start an

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index eeef8ff2d27e172c3083b5619d5fae62608f0afc..d9b6219b2d159032f13af762923a069794f7e6c8 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -38,12 +38,13 @@ let get_current_status_as_xml () =
   match get_proof () with
      None -> assert false
    | Some (uri, metasenv, bo, ty) ->
+      let uri = match uri with Some uri -> uri | None -> assert false in
       let currentproof =
        (*CSC: Wrong: [] is just plainly wrong *)
        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
       in
        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
-        Cic2acic.acic_object_of_cic_object currentproof
+        Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
        in
         let xml, bodyxml =
          match
@@ -61,7 +62,7 @@ let apply_tactic ~tactic =
   | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
-     let (newproof, newgoals) = tactic ~status:(proof', goal') in
+     let (newproof, newgoals) = tactic (proof', goal') in
       set_proof (Some newproof);
       goal :=
        (match newgoals, newproof with
@@ -83,7 +84,7 @@ let metas_in_term term =
       C.Rel _ -> []
     | C.Meta (n,_) -> [n]
     | C.Sort _
-    | C.Implicit -> []
+    | C.Implicit _ -> []
     | C.Cast (te,ty) -> (aux te) @ (aux ty)
     | C.Prod (_,s,t) -> (aux s) @ (aux t)
     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
@@ -121,11 +122,13 @@ let perforate context term ty =
   match get_proof () with
      None -> assert false
    | Some (uri,metasenv,bo,gty as proof') ->
-      let newmeta = new_meta proof' in
+      let newmeta = new_meta_of_proof proof' in
        (* We push the new meta at the end of the list for pretty-printing *)
        (* purposes: in this way metas are ordered.                        *)
        let metasenv' = metasenv@[newmeta,context,ty] in
-        let irl = identity_relocation_list_for_metavariable context in
+        let irl =
+          CicMkImplicit.identity_relocation_list_for_metavariable context
+        in
 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
         let bo' =
          ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
@@ -223,6 +226,7 @@ let fold_simpl term =
 let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
 let fourier () = apply_tactic FourierR.fourier_tac
+let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
 
 let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
 let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)