X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=a9b46267f98c9ba1a032ce6a9315aac3d04cadfe;hb=d1126c6b78a3333bbf415daf027004496b77c2f4;hp=fe9ea94d66b3ba1dafab5310c035217dcb5f164a;hpb=ee69e02cdf70e8fed61c3bf1c8f165b4798ad9fb;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index fe9ea94d6..a9b46267f 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -27,7 +27,8 @@ open Printf
 open MatitaTypes
 
 exception Drop;;
-exception UnableToInclude of string;;
+exception UnableToInclude of string
+exception IncludedFileNotCompiled of string
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
@@ -39,7 +40,9 @@ type options = {
 }
 
 type statement =
-  (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
+  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+   string)
+  GrafiteAst.statement
 
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
@@ -55,11 +58,13 @@ let namer_of names =
     end else
       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
-let tactic_of_ast = function
+let tactic_of_ast ast =
+  let module PET = ProofEngineTypes in
+  match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *)
+  | GrafiteAst.Auto (_,depth,width,paramodulation) ->
       AutoTactic.auto_tac ?depth ?width ?paramodulation
         ~dbd:(MatitaDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
@@ -84,24 +89,36 @@ let tactic_of_ast = function
       Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
-      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
+      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+        what
   | GrafiteAst.ElimType (_, what, using, depth, names) ->
-      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
+      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+        what
   | GrafiteAst.Exact (_, term) -> Tactics.exact term
   | GrafiteAst.Exists _ -> Tactics.exists
   | GrafiteAst.Fail _ -> Tactics.fail
   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
-     let reduction =
-      match reduction_kind with
-       | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
-       | `Reduce -> ProofEngineReduction.reduce
-       | `Simpl -> ProofEngineReduction.simpl
-       | `Whd -> CicReduction.whd ~delta:false ~subst:[]
-     in
+      let reduction =
+        match reduction_kind with
+        | `Normalize ->
+            PET.const_lazy_reduction
+              (CicReduction.normalize ~delta:false ~subst:[])
+        | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
+        | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
+        | `Unfold None ->
+            PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
+        | `Unfold (Some lazy_term) ->
+           (fun context metasenv ugraph ->
+             let what, metasenv, ugraph = lazy_term context metasenv ugraph in
+             ProofEngineReduction.unfold ~what, metasenv, ugraph)
+        | `Whd ->
+            PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[])
+      in
       Tactics.fold ~reduction ~term ~pattern
   | GrafiteAst.Fourier _ -> Tactics.fourier
   | GrafiteAst.FwdSimpl (_, hyp, names) -> 
-     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
+      ~dbd:(MatitaDb.instance ()) hyp
   | GrafiteAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
@@ -114,8 +131,9 @@ let tactic_of_ast = function
       PrimitiveTactics.intros_tac ~howmany:num
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
-     let names = match ident with None -> [] | Some id -> [id] in
-     Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
+      let names = match ident with None -> [] | Some id -> [id] in
+      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
+        ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
@@ -124,6 +142,7 @@ let tactic_of_ast = function
       | `Normalize -> Tactics.normalize ~pattern
       | `Reduce -> Tactics.reduce ~pattern  
       | `Simpl -> Tactics.simpl ~pattern 
+      | `Unfold what -> Tactics.unfold ~pattern what
       | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->
@@ -136,159 +155,190 @@ let tactic_of_ast = function
   | GrafiteAst.Symmetry _ -> Tactics.symmetry
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
 
-let disambiguate_term status term =
+let singleton = function
+  | [x] -> x
+  | _ -> assert false
+
+let disambiguate_term status_ref term =
+  let status = !status_ref in
   let (aliases, metasenv, cic, _) =
-    match
-      MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+    singleton
+      (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
-        ~metasenv:(MatitaMisc.get_proof_metasenv status) term
-    with
-    | [x] -> x
-    | _ -> assert false
+        ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
   in
-  let proof_status =
-    match status.proof_status with
-    | No_proof -> Intermediate metasenv
-    | Incomplete_proof ((uri, _, proof, ty), goal) ->
-        Incomplete_proof ((uri, metasenv, proof, ty), goal)
-    | Intermediate _ -> Intermediate metasenv 
-    | Proof _ -> assert false
-  in
-  let status = { status with proof_status = proof_status } in
+  let status = MatitaTypes.set_metasenv metasenv status in
   let status = MatitaSync.set_proof_aliases status aliases in
-  status, cic
+  status_ref := status;
+  cic
   
-let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
-  let interp path = Disambiguate.interpretate_path [] status.aliases path in
+  (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
+   * rationale: lazy_term will be invoked in different context to obtain a term,
+   * each invocation will disambiguate the term and can add aliases. Once all
+   * disambiguations have been performed, the first returned function can be
+   * used to obtain the resulting aliases *)
+let disambiguate_lazy_term status_ref term =
+  (fun context metasenv ugraph ->
+    let status = !status_ref in
+    let (aliases, metasenv, cic, ugraph) =
+      singleton
+        (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+          ~initial_ugraph:ugraph ~aliases:status.aliases ~context ~metasenv
+            term)
+    in
+    let status = MatitaTypes.set_metasenv metasenv status in
+    let status = MatitaSync.set_proof_aliases status aliases in
+    status_ref := status;
+    cic, metasenv, ugraph)
+
+let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
+  let interp path =
+    Disambiguate.interpretate_path [] !status_ref.aliases path
+  in
   let goal_path = interp goal_path in
   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
-  let status,wanted =
+  let wanted =
    match wanted with
-      None -> status,None
+      None -> None
     | Some wanted ->
-       let status,wanted = disambiguate_term status wanted in
-        status, Some wanted
+       let wanted = disambiguate_lazy_term status_ref wanted in
+       Some wanted
   in
-   status, (wanted, hyp_paths ,goal_path)
+  (wanted, hyp_paths ,goal_path)
+
+let disambiguate_reduction_kind aliases_ref = function
+  | `Unfold (Some t) ->
+      let t = disambiguate_lazy_term aliases_ref t in
+      `Unfold (Some t)
+  | `Normalize
+  | `Reduce
+  | `Simpl
+  | `Unfold None
+  | `Whd as kind -> kind
   
-let disambiguate_tactic status = function
-  | GrafiteAst.Apply (loc, term) ->
-      let status, cic = disambiguate_term status term in
-      status, GrafiteAst.Apply (loc, cic)
-  | GrafiteAst.Absurd (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, GrafiteAst.Absurd (loc, cic)
-  | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
-  | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *)
-  | GrafiteAst.Change (loc, pattern, with_what) -> 
-      let status, with_what = disambiguate_term status with_what in
-      let status, pattern = disambiguate_pattern status pattern in
-      status, GrafiteAst.Change (loc, pattern, with_what)
-  | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id)
-  | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id)
-  | GrafiteAst.Compare (loc,term) ->
-      let status, term = disambiguate_term status term in
-      status, GrafiteAst.Compare (loc,term)
-  | GrafiteAst.Constructor (loc,n) ->
-      status, GrafiteAst.Constructor (loc,n)
-  | GrafiteAst.Contradiction loc ->
-      status, GrafiteAst.Contradiction loc
-  | GrafiteAst.Cut (loc, ident, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, GrafiteAst.Cut (loc, ident, cic)
-  | GrafiteAst.DecideEquality loc ->
-      status, GrafiteAst.DecideEquality loc
-  | GrafiteAst.Decompose (loc, types, what, names) ->
-      let disambiguate (status, types) = function
-         | GrafiteAst.Type _   -> assert false
-	 | GrafiteAst.Ident id ->
-	    match disambiguate_term status (CicNotationPt.Ident (id, None)) with
-	       | status, Cic.MutInd (uri, tyno, _) ->
-	          status, (GrafiteAst.Type (uri, tyno) :: types)
-               | _                                 -> 
-	          raise Disambiguate.NoWellTypedInterpretation
-      in
-      let status, types = List.fold_left disambiguate (status, []) types in
-      status, GrafiteAst.Decompose(loc, types, what, names)  
-  | GrafiteAst.Discriminate (loc,term) ->
-      let status,term = disambiguate_term status term in
-      status, GrafiteAst.Discriminate(loc,term)
-  | GrafiteAst.Exact (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, GrafiteAst.Exact (loc, cic)
-  | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      let status, using = disambiguate_term status using in
-      status, GrafiteAst.Elim (loc, what, Some using, depth, idents)
-  | GrafiteAst.Elim (loc, what, None, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      status, GrafiteAst.Elim (loc, what, None, depth, idents)
-  | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      let status, using = disambiguate_term status using in
-      status, GrafiteAst.ElimType (loc, what, Some using, depth, idents)
-  | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      status, GrafiteAst.ElimType (loc, what, None, depth, idents)
-  | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc 
-  | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
-  | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
-     let status, pattern = disambiguate_pattern status pattern in
-     let status, term = disambiguate_term status term in
-     status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
-  | GrafiteAst.FwdSimpl (loc, hyp, names) ->
-     status, GrafiteAst.FwdSimpl (loc, hyp, names)  
-  | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
-  | GrafiteAst.Generalize (loc,pattern,ident) ->
-      let status, pattern = disambiguate_pattern status pattern in
-      status, GrafiteAst.Generalize(loc,pattern,ident)
-  | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g)
-  | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc
-  | GrafiteAst.Injection (loc,term) ->
-      let status, term = disambiguate_term status term in
-      status, GrafiteAst.Injection (loc,term)
-  | GrafiteAst.Intros (loc, num, names) ->
-      status, GrafiteAst.Intros (loc, num, names)
-  | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
-     let f term (status, to_what) =
-        let status, term = disambiguate_term status term in
-        status, term :: to_what
-     in
-     let status, to_what = List.fold_right f to_what (status, []) in 
-     let status, what = disambiguate_term status what in
-     status, GrafiteAst.LApply (loc, depth, to_what, what, ident)
-  | GrafiteAst.Left loc -> status, GrafiteAst.Left loc
-  | GrafiteAst.LetIn (loc, term, name) ->
-      let status, term = disambiguate_term status term in
-      status, GrafiteAst.LetIn (loc,term,name)
-  | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
-      let status, pattern = disambiguate_pattern status pattern in
-      status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
-  | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
-  | GrafiteAst.Replace (loc, pattern, with_what) -> 
-      let status, pattern = disambiguate_pattern status pattern in
-      let status, with_what = disambiguate_term status with_what in
-      status, GrafiteAst.Replace (loc, pattern, with_what)
-  | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
-      let status, term = disambiguate_term status t in
-      let status, pattern = disambiguate_pattern status pattern in
-      status, GrafiteAst.Rewrite (loc, dir, term, pattern)
-  | GrafiteAst.Right loc -> status, GrafiteAst.Right loc
-  | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc
-  | GrafiteAst.Split loc -> status, GrafiteAst.Split loc
-  | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc
-  | GrafiteAst.Transitivity (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, GrafiteAst.Transitivity (loc, cic)
+let disambiguate_tactic status tactic =
+  let status_ref = ref status in
+  let tactic =
+    match tactic with
+    | GrafiteAst.Absurd (loc, term) -> 
+        let cic = disambiguate_term status_ref term in
+        GrafiteAst.Absurd (loc, cic)
+    | GrafiteAst.Apply (loc, term) ->
+        let cic = disambiguate_term status_ref term in
+        GrafiteAst.Apply (loc, cic)
+    | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
+    | GrafiteAst.Auto (loc,depth,width,paramodulation) ->
+        GrafiteAst.Auto (loc,depth,width,paramodulation)
+    | GrafiteAst.Change (loc, pattern, with_what) -> 
+        let with_what = disambiguate_lazy_term status_ref with_what in
+        let pattern = disambiguate_pattern status_ref pattern in
+        GrafiteAst.Change (loc, pattern, with_what)
+    | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
+    | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
+    | GrafiteAst.Compare (loc,term) ->
+        let term = disambiguate_term status_ref term in
+        GrafiteAst.Compare (loc,term)
+    | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
+    | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
+    | GrafiteAst.Cut (loc, ident, term) -> 
+        let cic = disambiguate_term status_ref term in
+        GrafiteAst.Cut (loc, ident, cic)
+    | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
+    | GrafiteAst.Decompose (loc, types, what, names) ->
+        let disambiguate types = function
+           | GrafiteAst.Type _   -> assert false
+           | GrafiteAst.Ident id ->
+              (match disambiguate_term status_ref (CicNotationPt.Ident (id, None)) with
+              | Cic.MutInd (uri, tyno, _) ->
+                  (GrafiteAst.Type (uri, tyno) :: types)
+              | _ -> raise Disambiguate.NoWellTypedInterpretation)
+        in
+        let types = List.fold_left disambiguate [] types in
+        GrafiteAst.Decompose (loc, types, what, names)
+    | GrafiteAst.Discriminate (loc,term) ->
+        let term = disambiguate_term status_ref term in
+        GrafiteAst.Discriminate(loc,term)
+    | GrafiteAst.Exact (loc, term) -> 
+        let cic = disambiguate_term status_ref term in
+        GrafiteAst.Exact (loc, cic)
+    | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
+        let what = disambiguate_term status_ref what in
+        let using = disambiguate_term status_ref using in
+        GrafiteAst.Elim (loc, what, Some using, depth, idents)
+    | GrafiteAst.Elim (loc, what, None, depth, idents) ->
+        let what = disambiguate_term status_ref what in
+        GrafiteAst.Elim (loc, what, None, depth, idents)
+    | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+        let what = disambiguate_term status_ref what in
+        let using = disambiguate_term status_ref using in
+        GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+    | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+        let what = disambiguate_term status_ref what in
+        GrafiteAst.ElimType (loc, what, None, depth, idents)
+    | GrafiteAst.Exists loc -> GrafiteAst.Exists loc 
+    | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
+    | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
+        let pattern = disambiguate_pattern status_ref pattern in
+        let term = disambiguate_lazy_term status_ref term in
+        let red_kind = disambiguate_reduction_kind status_ref red_kind in
+        GrafiteAst.Fold (loc, red_kind, term, pattern)
+    | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+       GrafiteAst.FwdSimpl (loc, hyp, names)  
+    | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
+    | GrafiteAst.Generalize (loc,pattern,ident) ->
+        let pattern = disambiguate_pattern status_ref pattern in
+        GrafiteAst.Generalize (loc,pattern,ident)
+    | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
+    | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
+    | GrafiteAst.Injection (loc, term) ->
+        let term = disambiguate_term status_ref term in
+        GrafiteAst.Injection (loc,term)
+    | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+    | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+       let f term to_what =
+          let term = disambiguate_term status_ref term in
+          term :: to_what
+       in
+       let to_what = List.fold_right f to_what [] in 
+       let what = disambiguate_term status_ref what in
+       GrafiteAst.LApply (loc, depth, to_what, what, ident)
+    | GrafiteAst.Left loc -> GrafiteAst.Left loc
+    | GrafiteAst.LetIn (loc, term, name) ->
+        let term = disambiguate_term status_ref term in
+        GrafiteAst.LetIn (loc,term,name)
+    | GrafiteAst.Reduce (loc, red_kind, pattern) ->
+        let pattern = disambiguate_pattern status_ref pattern in
+        let red_kind = disambiguate_reduction_kind status_ref red_kind in
+        GrafiteAst.Reduce(loc, red_kind, pattern)
+    | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
+    | GrafiteAst.Replace (loc, pattern, with_what) -> 
+        let pattern = disambiguate_pattern status_ref pattern in
+        let with_what = disambiguate_lazy_term status_ref with_what in
+        GrafiteAst.Replace (loc, pattern, with_what)
+    | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+        let term = disambiguate_term status_ref t in
+        let pattern = disambiguate_pattern status_ref pattern in
+        GrafiteAst.Rewrite (loc, dir, term, pattern)
+    | GrafiteAst.Right loc -> GrafiteAst.Right loc
+    | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
+    | GrafiteAst.Split loc -> GrafiteAst.Split loc
+    | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+    | GrafiteAst.Transitivity (loc, term) -> 
+        let cic = disambiguate_term status_ref term in
+        GrafiteAst.Transitivity (loc, cic)
+  in
+  status_ref, tactic
 
 let apply_tactic tactic status =
- let status,tactic = disambiguate_tactic status tactic in
+ let status_ref, tactic = disambiguate_tactic status tactic in
+ let proof_status = MatitaMisc.get_proof_status !status_ref in
  let tactic = tactic_of_ast tactic in
- let (proof, goals) =
-  ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in
+ (* apply tactic will change the status pointed by status_ref ... *)
+ let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in
  let dummy = -1 in
-  { status with
-     proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals
+ { !status_ref with
+    proof_status = MatitaTypes.Incomplete_proof (proof,dummy) },
+ goals
 
 module MatitaStatus =
  struct
@@ -436,8 +486,6 @@ let generate_projections uri fields status =
      try 
       let ty, ugraph = 
         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
-      let bo = Unshare.unshare bo in
-      let ty = Unshare.unshare ty in
       let attrs = [`Class `Projection; `Generated] in
       let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
        MatitaSync.add_obj uri obj status
@@ -476,8 +524,8 @@ let disambiguate_obj status obj =
     match status.proof_status with
     | No_proof -> Intermediate metasenv
     | Incomplete_proof _
-    | Intermediate _
-    | Proof _ -> assert false
+    | Proof _ -> command_error "imbricated proofs not allowed"
+    | Intermediate _ -> assert false
   in
   let status = { status with proof_status = proof_status } in
   let status = MatitaSync.set_proof_aliases status aliases in
@@ -496,25 +544,27 @@ let disambiguate_command status = function
   | GrafiteAst.Set _ as cmd ->
       status,cmd
   | GrafiteAst.Coercion (loc, term) ->
-      let status, term = disambiguate_term status term in
-      status, GrafiteAst.Coercion (loc,term)
+      let status_ref = ref status in
+      let term = disambiguate_term status_ref term in
+      !status_ref, GrafiteAst.Coercion (loc,term)
   | GrafiteAst.Obj (loc,obj) ->
       let status,obj = disambiguate_obj status obj in
-       status, GrafiteAst.Obj (loc,obj)
+      status, GrafiteAst.Obj (loc,obj)
 
 let make_absolute paths path =
-  let rec aux = function
-  | [] -> ignore (Unix.stat path); path
-  | p :: tl ->
-     let path = p ^ "/" ^ path in
-      try
-        ignore (Unix.stat path); path
-      with Unix.Unix_error _ -> aux tl
-  in
-  try
-    aux paths
-  with Unix.Unix_error _ as exc ->
-    command_error ("File " ^ path ^ " not found")
+  if path = "coq.ma" then path
+  else
+   let rec aux = function
+   | [] -> ignore (Unix.stat path); path
+   | p :: tl ->
+      let path = p ^ "/" ^ path in
+       try
+         ignore (Unix.stat path); path
+       with Unix.Unix_error _ -> aux tl
+   in
+   try
+     aux paths
+   with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
 let eval_command opts status cmd =
@@ -532,7 +582,8 @@ let eval_command opts status cmd =
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
      let ic =
-      try open_in moopath with Sys_error _ -> raise (UnableToInclude moopath) in
+      try open_in moopath with Sys_error _ -> 
+        raise (IncludedFileNotCompiled moopath) in
      let stream = Stream.of_channel ic in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());
@@ -581,6 +632,8 @@ let eval_command opts status cmd =
       eval_coercion status coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let aliases =
+      (*CSC: Warning: this code should be factorized with the corresponding
+             code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
          DisambiguateTypes.Environment.add