X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=bf39a1caca2170658880b4673bd77b2c7bd7a874;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9595df9317714358a1de9e3f1a0f3fbedc0959db;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 9595df931..bf39a1cac 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -161,13 +161,13 @@ let disambiguate_term ?context status_ref goal term =
   let context =
     match context with
     | Some c -> c
-    | None -> MatitaMisc.get_proof_context status goal
+    | None -> MatitaTypes.get_proof_context status goal
   in
   let (diff, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases)
-        ~context ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
+        ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term)
   in
   let status = MatitaTypes.set_metasenv metasenv status in
   let status = MatitaSync.set_proof_aliases status diff in
@@ -253,7 +253,7 @@ let disambiguate_tactic status goal tactic =
               with
               | Cic.MutInd (uri, tyno, _) ->
                   (GrafiteAst.Type (uri, tyno) :: types)
-              | _ -> raise Disambiguate.NoWellTypedInterpretation)
+              | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
         in
         let types = List.fold_left disambiguate [] types in
         GrafiteAst.Decompose (loc, types, what, names)
@@ -455,13 +455,13 @@ let classify_tactic tactic =
   
 let apply_tactic tactic (status, goal) =
 (* prerr_endline "apply_tactic"; *)
-(* prerr_endline (Continuationals.Stack.pp (MatitaMisc.get_stack status)); *)
- let starting_metasenv = MatitaMisc.get_proof_metasenv status in
+(* prerr_endline (Continuationals.Stack.pp (MatitaTypes.get_stack status)); *)
+ let starting_metasenv = MatitaTypes.get_proof_metasenv status in
  let before = List.map (fun g, _, _ -> g) starting_metasenv in
 (* prerr_endline "disambiguate"; *)
  let status_ref, tactic = disambiguate_tactic status goal tactic in
- let metasenv_after_refinement =  MatitaMisc.get_proof_metasenv !status_ref in
- let proof = MatitaMisc.get_current_proof !status_ref in
+ let metasenv_after_refinement =  MatitaTypes.get_proof_metasenv !status_ref in
+ let proof = MatitaTypes.get_current_proof !status_ref in
  let proof_status = proof, goal in
  let needs_reordering, always_opens_a_goal = classify_tactic tactic in
  let tactic = tactic_of_ast tactic in
@@ -515,10 +515,10 @@ struct
   let apply_tactic tac = tac
   let goals (_, opened, closed) = opened, closed
   let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
-  let get_stack (status, _) = MatitaMisc.get_stack status
+  let get_stack (status, _) = MatitaTypes.get_stack status
 
   let set_stack stack (status, opened, closed) = 
-    MatitaMisc.set_stack stack status, opened, closed
+    MatitaTypes.set_stack stack status, opened, closed
 
   let inject (status, _) = (status, [], [])
   let focus goal (status, _, _) = (status, goal)
@@ -614,8 +614,11 @@ let eval_coercion status coercion =
   let new_coercions =
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
   let status =
-   List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
+   List.fold_left (fun s (uri,o,_) -> 
+      let status = MatitaSync.add_obj uri o status in
+      {status with coercions = uri :: status.coercions})
     status new_coercions in
+  let status = {status with coercions = coer_uri :: status.coercions} in
   let statement_of name =
     GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
       (CicNotationPt.Ident (name, None)))
@@ -675,7 +678,7 @@ let disambiguate_obj status obj =
    match obj with
       GrafiteAst.Inductive (_,(name,_,_,_)::_)
     | GrafiteAst.Record (_,name,_,_) ->
-       Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
+       Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind"))
     | GrafiteAst.Inductive _ -> assert false
     | GrafiteAst.Theorem _ -> None in
   let (diff, metasenv, cic, _) =
@@ -744,7 +747,7 @@ let eval_command opts status cmd =
      add_moo_content [cmd] status
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
-     let moopath = MatitaMisc.obj_file_of_script absolute_path in
+     let moopath = MatitacleanLib.obj_file_of_script absolute_path in
      let status = ref status in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
@@ -836,9 +839,9 @@ let eval_command opts status cmd =
           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
        | _ -> assert false in
      let uri = 
-       UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext) 
+       UriManager.uri_of_string (MatitaTypes.qualify status name ^ ext) 
      in
-     let metasenv = MatitaMisc.get_proof_metasenv status in
+     let metasenv = MatitaTypes.get_proof_metasenv status in
      match obj with
      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
          let name = UriManager.name_of_uri uri in
@@ -1015,6 +1018,7 @@ let initial_status =
     proof_status = No_proof;
     options = default_options ();
     objects = [];
+    coercions = [];
     notation_ids = [];
   }