]> matita.cs.unibo.it Git - helm.git/commitdiff
added a (for the moment) dummy field _subst to ProofengineTypes.proof.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 May 2007 17:22:37 +0000 (17:22 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 May 2007 17:22:37 +0000 (17:22 +0000)
36 file touched ;-)

33 files changed:
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/tactics/auto.ml
helm/software/components/tactics/autoTactic.ml
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/discriminationTactics.ml
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/fourierR.ml
helm/software/components/tactics/fwdSimplTactic.ml
helm/software/components/tactics/introductionTactics.ml
helm/software/components/tactics/inversion.ml
helm/software/components/tactics/inversion_principle.ml
helm/software/components/tactics/metadataQuery.ml
helm/software/components/tactics/negationTactics.ml
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/components/tactics/proofEngineStructuralRules.ml
helm/software/components/tactics/proofEngineTypes.ml
helm/software/components/tactics/proofEngineTypes.mli
helm/software/components/tactics/reductionTactics.ml
helm/software/components/tactics/ring.ml
helm/software/components/tactics/setoids.ml
helm/software/components/tactics/statefulProofEngine.ml
helm/software/components/tactics/substTactic.ml
helm/software/components/tactics/tacticals.ml
helm/software/components/tactics/variousTactics.ml
helm/software/matita/matita.ml
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaScript.ml
helm/software/matita/matitaWiki.ml

index 296625a1dbc43a7284a3f9d730cf671aa01db5e3..c961c58ae611903b2d518dfbf57b2b23ca5a1202 100644 (file)
@@ -332,14 +332,14 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
  let after = ProofEngineTypes.goals_of_proof proof in
  let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
  let proof, opened_goals = 
-  let uri, metasenv_after_tactic, t, ty, attrs = proof in
+  let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
   let reordered_metasenv, opened_goals = 
     reorder_metasenv
      starting_metasenv
      metasenv_after_refinement metasenv_after_tactic
      opened goal always_opens_a_goal
   in
-  let proof' = uri, reordered_metasenv, t, ty, attrs in
+  let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
   proof', opened_goals
  in
  let incomplete_proof =
@@ -366,14 +366,14 @@ let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (
  let after = ProofEngineTypes.goals_of_proof proof in
  let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
  let proof, opened_goals = 
-  let uri, metasenv_after_tactic, t, ty, attrs = proof in
+  let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
   let reordered_metasenv, opened_goals = 
     reorder_metasenv
      starting_metasenv
      metasenv_after_refinement metasenv_after_tactic
      opened goal always_opens_a_goal
   in
-  let proof' = uri, reordered_metasenv, t, ty, attrs in
+  let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
   proof', opened_goals
  in
  let incomplete_proof =
@@ -681,16 +681,16 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 *)
      status,[]
   | GrafiteAst.Print (_,"proofterm") ->
-      let _,_,p,_, _ = GrafiteTypes.get_current_proof status in
+      let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
       print_endline (AutoTactic.pp_proofterm p);
       status,[]
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Qed loc ->
-      let uri, metasenv, bo, ty, attrs =
+      let uri, metasenv, _subst, bo, ty, attrs =
         match status.GrafiteTypes.proof_status with
-        | GrafiteTypes.Proof (Some uri, metasenv, body, ty, attrs) ->
-            uri, metasenv, body, ty, attrs
-        | GrafiteTypes.Proof (None, metasenv, body, ty, attrs) -> 
+        | GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) ->
+            uri, metasenv, subst, body, ty, attrs
+        | GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) -> 
             raise (GrafiteTypes.Command_error 
               ("Someone allows to start a theorem without giving the "^
                "name/uri. This should be fixed!"))
@@ -787,7 +787,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
                   "\nPlease use a variant."));
            end;
-         let initial_proof = (Some uri, metasenv', bo, ty, attrs) in
+         let _subst = [] in
+         let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in
          let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
          { status with GrafiteTypes.proof_status =
             GrafiteTypes.Incomplete_proof
index fe872c128283332a31d83037693e9e9027b89bda..6e8be22bbe0367d149bdf148fbea77d8d9421395 100644 (file)
@@ -69,8 +69,8 @@ let get_current_proof status =
 let get_proof_metasenv status =
   match status.proof_status with
   | No_proof -> []
-  | Proof (_, metasenv, _, _, _)
-  | Incomplete_proof { proof = (_, metasenv, _, _, _) }
+  | Proof (_, metasenv, _, _, _, _)
+  | Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
   | Intermediate metasenv ->
       metasenv
 
@@ -93,11 +93,11 @@ let set_metasenv metasenv status =
   let proof_status =
     match status.proof_status with
     | No_proof -> Intermediate metasenv
-    | Incomplete_proof ({ proof = (uri, _, proof, ty, attrs) } as incomplete_proof) ->
+    | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
         Incomplete_proof
-          { incomplete_proof with proof = (uri, metasenv, proof, ty, attrs) }
+          { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
     | Intermediate _ -> Intermediate metasenv 
-    | Proof (_, metasenv', _, _, _) ->
+    | Proof (_, metasenv', _, _, _, _) ->
        assert (metasenv = metasenv');
        status.proof_status
   in
@@ -105,14 +105,14 @@ let set_metasenv metasenv status =
 
 let get_proof_context status goal =
   match status.proof_status with
-  | Incomplete_proof { proof = (_, metasenv, _, _, _) } ->
+  | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
       let (_, context, _) = CicUtil.lookup_meta goal metasenv in
       context
   | _ -> []
 
 let get_proof_conclusion status goal =
   match status.proof_status with
-  | Incomplete_proof { proof = (_, metasenv, _, _, _) } ->
+  | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
       let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
       conclusion
   | _ -> raise (Statement_error "no ongoing proof")
index 3bec5b0444d47e53f6bab870eb6d6b5ad36dffd6..6f293ff4a8b56e298d262c5c4a8ff68032f314d8 100644 (file)
@@ -225,7 +225,7 @@ let empty_tables =
 let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
   (* the local cache in initially empty  *)
   let cache = AutoCache.cache_empty in
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _subst,_, _, _ = proof in
   let signature = MetadataQuery.signature_of metasenv goal in
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
@@ -368,7 +368,7 @@ let build_equalities auto context metasenv tables universe cache newmeta equatio
 let close_more tables maxmeta context status auto universe cache =
   let (active,passive,bag) = tables in
   let proof, goalno = status in
-  let _, metasenv,_,_, _ = proof in  
+  let _, metasenv,_subst,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
   let equations = retrieve_equations signature universe cache context in
   let eqs_and_types =
@@ -401,7 +401,7 @@ let find_context_equalities
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
@@ -468,8 +468,8 @@ let new_metasenv_and_unify_and_t
    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) 
  in
  let proof',oldmetasenv =
-  let (puri,metasenv,pbo,pty, attrs) = proof in
-   (puri,newmetasenv,pbo,pty, attrs),metasenv
+  let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
+   (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
  in
  let goal_for_paramod =
   match LibraryObjects.eq_URI () with
@@ -479,7 +479,10 @@ let new_metasenv_and_unify_and_t
  in
  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
+ let proof'' = 
+   let uri,_,_subst,p,ty, attrs = proof' in 
+   uri,metasenv_for_paramod,_subst,p,ty, attrs 
+ in
  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
  let proof''',goals =
   ProofEngineTypes.apply_tactic
@@ -504,7 +507,7 @@ let new_metasenv_and_unify_and_t
  | Some (_,proof''''',_), active,passive,_  ->
      subst,proof''''',
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-       ~newmetasenv:(let _,m,_,_, _ = proof''''' in m),  active, passive
+       ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m),  active, passive
 ;;
 
 let rec count_prods context ty =
@@ -516,7 +519,7 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -1011,7 +1014,7 @@ let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
   subst, metasenv
 ;;
 let mk_fake_proof metasenv (goalno,_,_) goalty context = 
-  None,metasenv,Cic.Meta(goalno,mk_irl context),goalty, [] 
+  None,metasenv,[],Cic.Meta(goalno,mk_irl context),goalty, [] 
 ;;
 let equational_case 
   tables maxm cache depth fake_proof goalno goalty subst context 
@@ -1033,7 +1036,7 @@ let equational_case
         with 
           | None, active, passive, maxmeta -> 
               [], (active,passive,bag), cache, maxmeta, flags
-          | Some(subst',(_,metasenv,proof,_, _),open_goals),active,
+          | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
             passive,maxmeta ->
               assert_subst_are_disjoint subst subst';
               let subst = subst@subst' in
@@ -1059,7 +1062,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,proof,_, _),open_goals ->
+            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals = 
@@ -1081,7 +1084,7 @@ let try_candidate
 =
   let ppterm = ppterm context in
   try 
-    let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
+    let subst', ((_,metasenv,_subst,_,_, _), open_goals), maxmeta =
       PrimitiveTactics.apply_with_subst 
         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) 
     in
@@ -1752,7 +1755,7 @@ let rec position_of i x = function
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   Saturation.reset_refs();
   let proof,goalno = status in 
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
   let eq_uri,tty = eq_and_ty_of_goal ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
@@ -1858,7 +1861,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
         ~target ~table ~subterms_only ~demod_table (proof,goal)
   | false -> 
       (* this is the real auto *)
-      let _,metasenv,_,_, _ = proof in
+      let _,metasenv,_subst,_,_, _ = proof in
       let _,context,goalty = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
@@ -1873,7 +1876,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
               auto_all_solutions universe cache 
         else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
-      let (_,oldmetasenv,_,_, _) = proof in
+      let (_,oldmetasenv,_subst,_,_, _) = proof in
       hint := None;
       let elem = 
         metasenv,[],1,[D (goal,flags.maxdepth,P)],[]
@@ -1890,7 +1893,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
             *)
             let proof,metasenv = 
             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-              proof goal (CicMetaSubst.apply_subst subst) metasenv
+              proof goal subst metasenv
             in
             let opened = 
               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
@@ -1915,7 +1918,7 @@ let eq_of_goal = function
 
 (* DEMODULATE *)
 let demodulate_tac ~dbd ~universe (proof,goal)= 
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let initgoal = [], [], ty in
@@ -1942,7 +1945,7 @@ let demodulate_tac ~dbd ~universe (proof,goal)=
       in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
-          (curi,extended_metasenv,pbo,pty, attrs),goal in
+          (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
         let (status,newgoals) = 
           ProofEngineTypes.apply_tactic 
             (PrimitiveTactics.apply_tac ~term:proofterm)
index 79cf52e65fa7bfe791474ef02e08a52c6530e5c6..12041b2bc28a5354867ee6ca292d580bd48abd72 100644 (file)
@@ -56,7 +56,7 @@ let search_theorems_in_context status =
   let module S = CicSubstitution in
   let module PET = ProofEngineTypes in 
   let module PT = PrimitiveTactics in 
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
     | [] -> []
@@ -89,7 +89,7 @@ let search_theorems_in_context status =
 
 
 let compare_goals proof goal1 goal2 =
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 
@@ -129,7 +129,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   if List.mem ty already_seen_goals then [] else
   let already_seen_goals = ty::already_seen_goals in
   let facts = (depth = 1) in  
-  let _,metasenv,p,_, _ = proof in
+  let _,metasenv,_subst, p,_, _ = proof in
     (* first of all we check if the goal has been already
        inspected *)
   assert (CicUtil.exists_meta goal metasenv);
@@ -148,12 +148,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
               (* if we just apply the subtitution, the type 
                  is irrelevant: we may use Implicit, since it will 
                  be dropped *)
-              CicMetaSubst.apply_subst 
-                [(goal,(ey, bo, Cic.Implicit None))] in
+                [(goal,(ey, bo, Cic.Implicit None))] 
+            in
+            let _ = assert false in
             let (proof,_) = 
               ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
                 proof goal subst_in metasenv in
-              [(subst_in,(proof,[],sign))]
+              [(CicMetaSubst.apply_subst subst_in,(proof,[],sign))]
         | No d when (d >= depth) -> 
             (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
             [] (* the empty list means no choices, i.e. failure *)
@@ -228,7 +229,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 and auto_new dbd width already_seen_goals universe = function
   | [] -> []
   | (subst,(proof, goals, sign))::tl ->
-      let _,metasenv,_,_, _ = proof in
+      let _,metasenv, _subst, _,_, _ = proof in
       let goals'=
         List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
@@ -244,7 +245,7 @@ and auto_new_aux dbd width already_seen_goals universe = function
       (List.length goals) > width -> 
       auto_new dbd width already_seen_goals universe tl 
   | (subst,(proof, (goal,depth)::gtl, sign))::tl -> 
-      let _,metasenv,p,_, _ = proof in
+      let _,metasenv,_subst,p,_, _ = proof in
       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
       match (auto_single dbd proof goal ey ty depth
         (width - (List.length gtl)) sign already_seen_goals) universe
@@ -284,7 +285,7 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
     | (_,(proof,[],_))::_ ->
         let t2 = Unix.gettimeofday () in
         debug_print (lazy "AUTO_TAC HA FINITO");
-        let _,_,p,_, _ = proof in
+        let _,_,_subst,p,_, _ = proof in
         debug_print (lazy (CicPp.ppterm p));
         debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
         (proof,[])
index e36c860374cc8e109ec4d35068b1d87f3ea8ce5f..2f012ed40d9eded87bf8fcf62c6c0dd929aafac6 100644 (file)
@@ -123,10 +123,10 @@ let we_need_to_prove t id ty =
 
 let existselim ~dbd ~universe t id1 t1 id2 t2 =
  let aux (proof, goal) = 
-  let (n,metasenv,bo,ty,attrs) = proof in
+  let (n,metasenv,_subst,bo,ty,attrs) = proof in
   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
-  let proof' = (n,metasenv,bo,ty,attrs) in
+  let proof' = (n,metasenv,_subst,bo,ty,attrs) in
    ProofEngineTypes.apply_tactic (
    Tacticals.thens
     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
@@ -155,7 +155,7 @@ let andelim t id1 t1 id2 t2 =
 
 let rewritingstep ~dbd ~universe lhs rhs just last_step =
  let aux ((proof,goal) as status) =
-  let (curi,metasenv,proofbo,proofty, attrs) = proof in
+  let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
   let _,context,gty = CicUtil.lookup_meta goal metasenv in
   let eq,trans =
    match LibraryObjects.eq_URI () with
@@ -221,7 +221,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
              FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
                (Cic.Name name) ~typ
            in
-            let proof = curi,metasenv,proofbo,proofty, attrs in
+            let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
             let proof,goals =
              ProofEngineTypes.apply_tactic
               (Tacticals.thens
index ccbf17ae643df6a099d7e99309da3c5356bd010e..9d83ad595e8af2dfa6712afcfb04b0415f6fb7ae 100644 (file)
@@ -145,7 +145,7 @@ let discriminate_tac ~term =
  in
  let discriminate'_tac ~term status = 
   let (proof, goal) = status in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
@@ -228,7 +228,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
  in
  let injection_tac ~term status = 
   let (proof, goal) = status in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst, _,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let term = CicSubstitution.lift liftno term in
   let termty,_ = 
@@ -335,7 +335,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
    * differiscono (o potrebbero differire?) nell'i-esimo parametro 
    * del costruttore *)
   let term = CicSubstitution.lift liftno term in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
@@ -467,7 +467,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                     (fun status ->    
                       debug_print (lazy "riempo il cut"); 
                       let (proof, goal) = status in
-                      let _,metasenv,_,_, _ = proof in
+                      let _,metasenv,_subst,_,_, _ = proof in
                       let _,context,gty =CicUtil.lookup_meta goal metasenv in
                       let gty = Unshare.unshare gty in
                       let new_t1' = 
index f18d2b333b68b322523b656db7db9527816c7324..29961db389d1c3a039b23286b4eb643f075a0146 100644 (file)
@@ -91,7 +91,7 @@ let rec check_type sorts metasenv context t =
 let rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
@@ -111,7 +111,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
 let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
    let elim_clear_unfold_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = PEH.lookup_type metasenv context what in
       let tac = 
@@ -159,7 +159,7 @@ let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp])
                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in
-      let _, metasenv,_,_, _ = proof in
+      let _, metasenv, _subst, _,_, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
       let old_context_length = List.length context in      
index f284a2d1d145dbdb6d2c49c6885098ae19904e9c..bd73865af94ffcf050498704a9be1be71543ff23 100644 (file)
@@ -44,7 +44,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
  let _rewrite_tac status =
   assert (wanted = None);   (* this should be checked syntactically *)
   let proof,goal = status in
-  let curi, metasenv, pbo, pty, attrs = proof in
+  let curi, metasenv, _subst, pbo, pty, attrs = proof in
   let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
   let gsort,_ =
    CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
@@ -196,7 +196,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   try 
     let (proof',goals) =
       PET.apply_tactic 
-        (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty, attrs),goal)
+        (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal)
     in
     let goals =
      goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
@@ -229,7 +229,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
  let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
   let _wanted, hyps_pat, concl_pat = pattern in
   let (proof, goal) = status in
-  let uri,metasenv,pbo,pty, attrs = proof in
+  let uri,metasenv,_subst,pbo,pty, attrs = proof in
   let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   assert (hyps_pat = []); (*CSC: not implemented yet *)
   let eq_URI =
@@ -246,7 +246,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let with_what = CicMetaSubst.apply_subst subst with_what in
   let pbo = CicMetaSubst.apply_subst subst pbo in
   let pty = CicMetaSubst.apply_subst subst pty in
-  let status = (uri,metasenv,pbo,pty, attrs),goal in
+  let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
   let ty_of_with_what,u =
    CicTypeChecker.type_of_aux'
     metasenv context with_what CicUniv.empty_ugraph in
@@ -288,7 +288,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
            (ProofEngineTypes.Fail
              (lazy "Replace: one of the selected terms and the term to be replaced with have not convertible types"))
        ) l in
-  let rec aux n whats status =
+  let rec aux n whats (status : ProofEngineTypes.status) =
    match whats with
       [] -> ProofEngineTypes.apply_tactic T.id_tac status
     | (what,lazy_pattern)::tl ->
@@ -313,7 +313,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
                     ~start:(
                       ProofEngineTypes.mk_tactic
                        (function ((proof,goal) as status) ->
-                         let _,metasenv,_,_, _ = proof in
+                         let _,metasenv,_subst,_,_, _ = proof in
                          let _,context,_ = CicUtil.lookup_meta goal metasenv in
                          let hyps =
                           try
@@ -328,7 +328,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
               T.id_tac])
          status
   and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in
-   aux 0 whats status
+   aux 0 whats (status : ProofEngineTypes.status)
  in
    ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what)
 ;;
@@ -342,7 +342,7 @@ let reflexivity_tac =
 
 let symmetry_tac =
  let symmetry_tac (proof, goal) =
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
@@ -360,7 +360,7 @@ let symmetry_tac =
 let transitivity_tac ~term =
  let transitivity_tac ~term status =
   let (proof, goal) = status in
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) 
index d9f0ce9a48f25e8eb9737ef51548b765dca72b30..8e443447a892f2a160fd7c724697698857a987b8 100644 (file)
@@ -577,7 +577,7 @@ let tac_zero_inf_pos (n,d) =
    (*let cste = pf_parse_constr gl in*)
    let pall str (proof,goal) t =
      debug ("tac "^str^" :\n" );
-     let curi,metasenv,pbo,pty, attrs = proof in
+     let curi,metasenv,_subst,pbo,pty, attrs = proof in
      let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      debug ("th = "^ CicPp.ppterm t ^"\n"); 
      debug ("ty = "^ CicPp.ppterm ty^"\n"); 
@@ -675,7 +675,7 @@ let tac_zero_inf_false gl (n,d) =
 let tac_zero_infeq_false gl (n,d) =
  let tac_zero_infeq_false gl (n,d) status =
   let (proof, goal) = status in
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   
   debug("faccio fold di " ^ CicPp.ppterm
@@ -713,13 +713,13 @@ let tac_zero_infeq_false gl (n,d) =
 
 let apply_type_tac ~cast:t ~applist:al = 
  let apply_type_tac ~cast:t ~applist:al (proof,goal) = 
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,t)::metasenv in
-   let proof' = curi,metasenv',pbo,pty, attrs in
+   let proof' = curi,metasenv',_subst,pbo,pty, attrs in
     let proof'',goals =
      apply_tactic 
       (PrimitiveTactics.apply_tac 
@@ -734,13 +734,13 @@ let apply_type_tac ~cast:t ~applist:al =
 
 let my_cut ~term:c =
  let my_cut ~term:c (proof,goal) =
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,c)::metasenv in
-   let proof' = curi,metasenv',pbo,pty, attrs in
+   let proof' = curi,metasenv',_subst,pbo,pty, attrs in
     let proof'',goals =
      apply_tactic 
       (apply_type_tac 
@@ -762,7 +762,7 @@ let tac_use h =
  let tac_use h status = 
   let (proof, goal) = status in
   debug("Inizio TC_USE\n");
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
   debug ("ty = "^ CicPp.ppterm ty^"\n");
@@ -873,7 +873,7 @@ let equality_replace a b =
  debug("inizio EQ\n");
   let module C = Cic in
    let proof,goal = status in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
@@ -886,7 +886,7 @@ let equality_replace a b =
        ~direction:`LeftToRight
        ~pattern:(ProofEngineTypes.conclusion_pattern None)
        (C.Meta (fresh_meta,irl)) [])
-     ((curi,metasenv',pbo,pty, attrs),goal)
+     ((curi,metasenv',_subst,pbo,pty, attrs),goal)
     in
     let new_goals = fresh_meta::goals in
  debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
@@ -934,7 +934,7 @@ let contradiction_tac (proof,goal)=
 (* ********************* TATTICA ******************************** *)
 
 let rec fourier (s_proof,s_goal)=
-  let s_curi,s_metasenv,s_pbo,s_pty, attrs = s_proof in
+  let s_curi,s_metasenv,_subst,s_pbo,s_pty, attrs = s_proof in
   let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
   debug_pcontext s_context;
@@ -974,7 +974,7 @@ let rec fourier (s_proof,s_goal)=
 
    (* now we have all the right environment *)
    
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
    (* now we want to convert hp to inequations, but first we must lift
@@ -1061,7 +1061,7 @@ let rec fourier (s_proof,s_goal)=
            (Tacticals.thens 
              ~start:(mk_tactic (fun status -> 
               debug ("inizio t1 strict\n");
-              let curi,metasenv,pbo,pty, attrs = proof in
+              let curi,metasenv,_subst,pbo,pty, attrs = proof in
               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
               debug ("ty = "^ CicPp.ppterm ty^"\n"); 
@@ -1092,7 +1092,7 @@ let rec fourier (s_proof,s_goal)=
              tac1:=(Tacticals.thens 
               ~start:(mk_tactic (fun status -> 
                 debug("INIZIO TAC 1 2\n");
-                let curi,metasenv,pbo,pty, attrs = proof in
+                let curi,metasenv,_subst,pbo,pty, attrs = proof in
                 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
                 debug ("ty = "^ CicPp.ppterm ty^"\n"); 
@@ -1128,7 +1128,7 @@ let rec fourier (s_proof,s_goal)=
          ~continuations:[Tacticals.then_  
            ~start:( mk_tactic (fun status ->
              let (proof, goal) = status in
-             let curi,metasenv,pbo,pty, attrs = proof in
+             let curi,metasenv,_subst,pbo,pty, attrs = proof in
              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              apply_tactic 
               (ReductionTactics.change_tac
@@ -1167,7 +1167,7 @@ let rec fourier (s_proof,s_goal)=
                 Tacticals.then_ 
                  ~start:(mk_tactic (fun status ->
                    let (proof, goal) = status in
-                   let curi,metasenv,pbo,pty, attrs = proof in
+                   let curi,metasenv,_subst,pbo,pty, attrs = proof in
                    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                    (* check if ty is of type *)
                    let w1 = 
index 60d43e7c7247f5407fb042c7e1fdb46caaf21c04..8734837d123917240513cb86cc7ab0bff14b06d2 100644 (file)
@@ -47,7 +47,7 @@ let error msg = raise (PET.Fail (lazy msg))
 let id_tac = 
    let id_tac (proof,goal) = 
       try
-         let _, metasenv, _, _, _ = proof in
+         let _, metasenv, _subst, _, _, _ = proof in
          let _, _, _ = CicUtil.lookup_meta goal metasenv in
          (proof,[goal])
       with CicUtil.Meta_not_found _ -> (proof, [])
@@ -62,7 +62,7 @@ let clearbody ~index =
    in
    let clearbody status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status
    in
@@ -109,7 +109,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name
                (* ?(substs = []) *) ?how_many ?(to_what = []) what =
    let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in   
    let lapply_tac (proof, goal) =
-      let xuri, metasenv, u, t, attrs = proof in
+      let xuri, metasenv, _subst, u, t, attrs = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
       let lemma = FNG.clean_dummy_dependent_types lemma in
@@ -121,7 +121,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name
         T.then_ ~start:(letin_tac conclusion) 
                  ~continuation:(clearbody ~index:1)     
       in
-      let proof = (xuri, metasenv, u, t, attrs) in
+      let proof = (xuri, metasenv, _subst, u, t, attrs) in
       let aux (proof, goals) (tac, goal) = 
          let proof, new_goals = PET.apply_tactic tac (proof, goal) in
         proof, goals @ new_goals
@@ -134,7 +134,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
                (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
    let lapply_tac status =
       let proof, goal = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
       let tac =  
@@ -159,7 +159,7 @@ let fwd_simpl_tac
    in
    let fwd_simpl_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
       let index, major = PEH.lookup_type metasenv context hyp in 
       match FwdQueries.fwd_simpl ~dbd major with
index 07a0c40b545d90cf7c400a0f73bd0e0094809b78..d8caf933ba5e986f6b67b65ac6ff154a65cf1dd7 100644 (file)
@@ -28,7 +28,7 @@
 let fake_constructor_tac ~n (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.MutInd (uri, typeno, exp_named_subst))
index 5f90c45ebbee4854c64ebe0e44c5883d7d1773ea..19d0c739ae87816ac9c26f6fded33d04f681ab37 100644 (file)
@@ -183,7 +183,7 @@ let private_inversion_tac ~term =
  let private_inversion_tac ~term (proof, goal) =
  
  (*DEBUG*) debug_print (lazy  ("private inversion begins"));
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
  let uri_of_eq =
   match LibraryObjects.eq_URI () with
      None -> raise EqualityNotDefinedYet
@@ -240,7 +240,7 @@ let private_inversion_tac ~term =
  (*DEBUG*) debug_print (lazy  ("after apply HCUT;reflexivity 
   in private inversion"));
  (* apply (ledx_ind( lambda x. lambda y, ...)) *)
- let t1,metasenv,t3,t4, attrs = proof2 in
+ let t1,metasenv,_subst,t3,t4, attrs = proof2 in
  let goal2 = List.hd (List.tl gl1) in
  let (_,context,_) = CicUtil.lookup_meta goal2 metasenv in
  (* rightparameters type list *)
@@ -265,13 +265,13 @@ let private_inversion_tac ~term =
  in
  (*DEBUG*) debug_print (lazy  ("private inversion: termine after refinement: "
   ^ CicPp.ppterm ref_t));
- let proof2 = (t1,metasenv'',t3,t4, attrs) in
+ let proof2 = (t1,metasenv'',_subst,t3,t4, attrs) in
  let my_apply_tac =
   let my_apply_tac status =
    let proof,goals = 
     ProofEngineTypes.apply_tactic (P.apply_tac ref_t) status in
    let patched_new_goals =
-    let (_,metasenv''',_,_, _) = proof in
+    let (_,metasenv''',_subst,_,_, _) = proof in
     let new_goals = ProofEngineHelpers.compare_metasenvs
      ~oldmetasenv:metasenv ~newmetasenv:metasenv''
     in
@@ -305,7 +305,7 @@ let inversion_tac ~term =
  let module PET = ProofEngineTypes in
  let inversion_tac ~term (proof, goal) =
  (*DEBUG*) debug_print (lazy ("inversion begins"));
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
   let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
   let uri, typeno = 
@@ -340,15 +340,15 @@ let inversion_tac ~term =
   Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
   in
   let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
-  let (t1,metasenv,t3,t4, attrs) = proof in
+  let (t1,metasenv,_subst,t3,t4, attrs) = proof in
   let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
   CicUniv.empty_ugraph 
   in
-  let proof = (t1,metasenv'',t3,t4, attrs) in
+  let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
   let proof3,gl3 = 
      ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in
   let patched_new_goals =
-     let (_,metasenv''',_,_, _) = proof3 in
+     let (_,metasenv''',_subst,_,_, _) = proof3 in
      let new_goals = ProofEngineHelpers.compare_metasenvs
       ~oldmetasenv:metasenv ~newmetasenv:metasenv''
      in
index b0f4d236ff5aa23e3fefad53b73e831c578e3274..45ece4823a95caf0d54d9cf578841830f1962c40 100644 (file)
@@ -154,8 +154,9 @@ let build_inversion uri obj =
             let goal = CicMkImplicit.new_meta metasenv [] in
             let metasenv' = (goal,[],ref_theorem)::metasenv in
             let attrs = [`Class (`InversionPrinciple); `Generated] in
+       let _subst = [] in
             let proof= 
-              (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in 
+              (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in 
             let _,applies =
               List.fold_right
                 (fun _ (i,applies) ->
@@ -186,7 +187,7 @@ let build_inversion uri obj =
                 (proof,goal) 
             in
             let metasenv,bo,ty, attrs =
-              match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs
+              match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
             in
               assert (metasenv = []);
               Some
index 2cfd95e9a96ed0cc71392f2bb36e64e42d68ee3e..6b87de349ce7f2225b54835e968b6cb54c7d6463 100644 (file)
@@ -109,7 +109,7 @@ let filter_uris_backward ~dbd ~facts signature uris =
     intersect uris siguris 
 
 let compare_goal_list proof goal1 goal2 =
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv, _subst, _,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = 
@@ -195,7 +195,7 @@ let cmatch' = Constr.cmatch'
 
 (* used only by te old auto *)
 let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
  let set = signature_of_hypothesis context metasenv in
@@ -344,7 +344,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
     ^ "\n}"
   in
 *)
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = 
    match signature with 
@@ -394,7 +394,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
 
 let experimental_hint 
   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
-  let (_, metasenv, _, _, _) = proof in
+  let (_, metasenv, _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
@@ -478,7 +478,7 @@ let new_experimental_hint
   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
-  let (_, metasenv, _, _, _) = proof in
+  let (_, metasenv,  _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
index e77fdf4de30269800c4ccf36b084ee2792fcdb30..fb904bf361df7025b2203cd615133dce4885d0b1 100644 (file)
@@ -31,7 +31,7 @@ let absurd_tac ~term =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let absurd_URI =
    match LibraryObjects.absurd_URI () with
index f8b12c11952051f3736ab24d314b6bc74aed15fd..f8b0ff45fcc088dcc5c799c93e8831c9be2f3b2b 100644 (file)
@@ -1319,7 +1319,7 @@ let build_proof
   if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
   else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let names = Utils.names_of_context context in
@@ -1394,7 +1394,7 @@ let build_proof
 *)
   let proof, real_metasenv = 
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-      proof goalno (CicMetaSubst.apply_subst final_subst) 
+      proof goalno final_subst
       (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
   in      
   let open_goals = 
@@ -1568,7 +1568,7 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
 let all_subsumed bag maxm status active passive =
   maxmeta := maxm;
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let env = metasenv,context,CicUniv.empty_ugraph in
   let cleaned_goal = Utils.remove_local_context type_of_goal in
@@ -1615,7 +1615,7 @@ let given_clause
   let mp = max_l passive_l in
 *)
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let cleaned_goal = Utils.remove_local_context type_of_goal in
index c5aab0f5ff45eeebb63f608195552302d799df26..aeb0c0751286285b637a1cff94aae6854ee3cae4 100644 (file)
@@ -261,7 +261,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -325,7 +325,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
               we may use Implicit, since it will be dropped *)
-     CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
+      ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
@@ -373,7 +373,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
  =
   let module C = Cic in
   let module R = CicReduction in
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
@@ -393,7 +393,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
@@ -428,7 +428,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    (* occur check *)
    let occur i t =
      let m = CicUtil.metas_of_term t in 
@@ -464,7 +464,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
 let exact_tac ~term =
  let exact_tac ~term (proof, goal) =
   (* Assumption: the term bo must be closed in the current context *)
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
@@ -497,7 +497,7 @@ module RT  = ReductionTactics
 let beta_after_elim_tac upto predicate =
    let beta_after_elim_tac status =
       let proof, goal = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, _, ty = CicUtil.lookup_meta goal metasenv in
       let mk_pattern ~equality ~upto ~predicate ty =
          (* code adapted from ProceduralConversion.generalize *)
@@ -564,7 +564,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       | _                    -> raise (PET.Fail (lazy "not implemented"))
    in    
    let ugraph = CicUniv.empty_ugraph in
-   let curi, metasenv, proofbo, proofty, attrs = proof in
+   let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
    let conjecture = CicUtil.lookup_meta goal metasenv in
    let metano, context, ty = conjecture in 
     let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
@@ -686,13 +686,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
          ProofEngineHelpers.compare_metasenvs
             ~oldmetasenv:metasenv ~newmetasenv:metasenv''
       in
-      let proof' = curi,metasenv'',proofbo,proofty, attrs in
+      let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
       let proof'', new_goals' =
          PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
       in
       (* The apply_tactic can have closed some of the new_goals *)
       let patched_new_goals =
-         let (_,metasenv''',_,_, _) = proof'' in
+         let (_,metasenv''',_subst,_,_, _) = proof'' in
          List.filter
             (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
            new_goals @ new_goals'
@@ -714,7 +714,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-  let (curi,metasenv,proofbo,proofty, attrs) = proof in
+  let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
   let termty = CicReduction.whd context termty in
@@ -825,13 +825,13 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     ProofEngineHelpers.compare_metasenvs
       ~oldmetasenv:metasenv ~newmetasenv:metasenv''
   in
-  let proof' = curi,metasenv'',proofbo,proofty, attrs in
+  let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
   let proof'', new_goals' =
     PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
   in
   (* The apply_tactic can have closed some of the new_goals *)
   let patched_new_goals =
-    let (_,metasenv''',_,_,_) = proof'' in
+    let (_,metasenv''',_subst,_,_,_) = proof'' in
       List.filter
         (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
         new_goals @ new_goals'
@@ -866,7 +866,7 @@ let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
    let letout_tac (proof, goal) =
-      let curi, metasenv, pbo, pty, attrs = proof in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
       let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
       let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
index 2a637135351516703b6e83e8c500ef467e11687a..85dba95ea1942859856ce77d0eaf042c25d5ca49 100644 (file)
 
 exception Bad_pattern of string Lazy.t
 
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _) =
+let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
   CicMkImplicit.new_meta metasenv []
 
 let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty, attrs = proof in
+ let uri,metasenv,initial_subst,bo,ty, attrs = proof in
    (* empty context is ok for term since it wont be used by apply_subst *)
    (* hack: since we do not know the context and the type of term, we
       create a substitution with cc =[] and type = Implicit; they will be
@@ -62,7 +62,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
       * since the parser does not reject as statements terms with
       * metavariable therein *)
      let ty' = subst_in ty in
-      let newproof = uri,metasenv'',bo',ty', attrs in
+      let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -77,8 +77,9 @@ let subst_meta_in_proof proof meta term newmetasenv =
 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
 (*CSC: [newmetasenv].                                             *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty, attrs) = proof in
+let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
+ let (uri,_,initial_subst,bo,ty, attrs) = proof in
+  let subst_in = CicMetaSubst.apply_subst subst in
   let bo' = subst_in bo in
   (* Metavariables can appear also in the *statement* of the theorem
    * since the parser does not reject as statements terms with
@@ -104,7 +105,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = uri,metasenv',bo',ty', attrs in
+  (* qui da capire se per la fase transitoria si fa initial_subst @ subst
+   * oppure subst *)
+   let newproof = uri,metasenv',subst,bo',ty', attrs in
     (newproof, metasenv')
 
 let compare_metasenvs ~oldmetasenv ~newmetasenv =
index 0a053ece7dcd212f1e37aef499ee6e6977529705..1eeb0aca3b3356a9168673d20750a35d8d05720e 100644 (file)
@@ -35,7 +35,7 @@ val subst_meta_in_proof :
   ProofEngineTypes.proof * Cic.metasenv
 val subst_meta_and_metasenv_in_proof :
   ProofEngineTypes.proof ->
-  int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
+  int -> Cic.substitution -> Cic.metasenv ->
   ProofEngineTypes.proof * Cic.metasenv
 
 (* returns the list of goals that are in newmetasenv and were not in
index 636ea07c0f3c67d36ba04ae3dc4057a6de4b14e5..ea7586e164f77c3a03079bdc9142481eb396ac70 100644 (file)
@@ -30,7 +30,7 @@ module C = Cic
 
 let clearbody ~hyp = 
  let clearbody (proof, goal) =
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
      let string_of_name =
       function
@@ -93,13 +93,13 @@ let clearbody ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty, attrs), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
   PET.mk_tactic clearbody
 
 let clear_one ~hyp =
  let clear_one (proof, goal) =
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,context,ty =
      CicUtil.lookup_meta goal metasenv
     in
@@ -151,7 +151,7 @@ let clear_one ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty, attrs), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
   PET.mk_tactic clear_one
 
@@ -176,7 +176,7 @@ let rename ~froms ~tos =
          try List.combine froms tos
         with Invalid_argument _ -> raise (PET.Fail (lazy error))
       in
-      let curi, metasenv, pbo, pty, attrs = proof in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
       let metano, _, _ = CicUtil.lookup_meta goal metasenv in      
       let rename_map = function
          | Some (Cic.Name hyp, decl_or_def) as entry ->
@@ -191,6 +191,6 @@ let rename ~froms ~tos =
          | conjecture -> conjecture
       in
       let metasenv = List.map map metasenv in
-      (curi, metasenv, pbo, pty, attrs), [goal]
+      (curi, metasenv, _subst, pbo, pty, attrs), [goal]
    in
    PET.mk_tactic rename
index eb48ff3e8d86902f8e114ab73f0b2d3af959e39f..abe460775b935a5271a6cda8a5deb8e1ac5a879f 100644 (file)
@@ -28,7 +28,7 @@
   (**
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
-type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list
+type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal
@@ -43,8 +43,9 @@ let initial_status ty metasenv attrs =
           aux max tl
   in
   let newmeta_idx = aux 0 metasenv in
+  let _subst = [] in
   let proof =
-    None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty, attrs
+    None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs
   in
   (proof, newmeta_idx)
 
@@ -90,13 +91,13 @@ exception Fail of string Lazy.t
     calls the opaque tactic on the status
   *)
 let apply_tactic t status = 
-  let (uri,metasenv,bo,ty, attrs), gl = t status in
+  let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
   match 
     CicRefine.pack_coercion_obj 
       (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
   with
   | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) -> 
-      (uri,metasenv,bo,ty, attrs), gl
+      (uri,metasenv,subst,bo,ty, attrs), gl
   | _ -> assert false
 ;;
 
@@ -104,5 +105,5 @@ let apply_tactic t status =
 type mk_fresh_name_type =
  Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
 
-let goals_of_proof (_,metasenv,_,_,_) = List.map (fun (g,_,_) -> g) metasenv
+let goals_of_proof (_,metasenv,_subst,_,_,_) = List.map (fun (g,_,_) -> g) metasenv
 
index f326a469f126cb65e376b66947c86280520d6bcb..6edcfeccc053a7559b715604e9a08f8c421a66f9 100644 (file)
@@ -27,7 +27,7 @@
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
 type proof =
- UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list
+ UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal
index 685baff9be8ecea7dfb4885ad9965bd8b7aa8199..3afef8eede4884141ab3c23aab3f79e73a842d61 100644 (file)
@@ -30,7 +30,7 @@ open ProofEngineTypes
 (* Note: this code is almost identical to change_tac and
 *  it could be unified by making the change function a callback *)
 let reduction_tac ~reduction ~pattern (proof,goal) =
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -88,7 +88,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
       | _ as t -> t
     ) metasenv
   in
-  (curi,metasenv',pbo,pty, attrs), [metano]
+  (curi,metasenv',_subst,pbo,pty, attrs), [metano]
 ;;
 
 let simpl_tac ~pattern =
@@ -137,7 +137,7 @@ exception NotConvertible
         term(s) to be replaced. *)
 let change_tac ~pattern with_what  =
  let change_tac ~pattern ~with_what (proof, goal) =
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let change subst where terms metasenv ugraph =
    if terms = [] then where, metasenv, ugraph
@@ -206,7 +206,7 @@ let change_tac ~pattern with_what  =
         | _ as t -> t)
       metasenv
   in
-  (curi,metasenv',pbo,pty, attrs), [metano]
+  (curi,metasenv',_subst,pbo,pty, attrs), [metano]
   in
     mk_tactic (change_tac ~pattern ~with_what)
 
index b2d3032706960ca8757588c695cdd16741f48ed2..7695a4ff0c82d885b66c9a76f1a3478cd915823b 100644 (file)
@@ -122,14 +122,14 @@ let cic_is_const ?(uri: uri option = None) term =
     @param proof a proof
     @return the uri of a given proof
   *)
-let uri_of_proof ~proof:(uri, _, _, _, _) = uri
+let uri_of_proof ~proof:(uri, _, _, _, _, _) = uri
 
   (**
     @param status current proof engine status
     @raise Failure if proof is None
     @return current goal's metasenv
   *)
-let metasenv_of_status ((_,m,_,_, _), _) = m
+let metasenv_of_status ((_,m,_,_,_, _), _) = m
 
   (**
     @param status a proof engine status
@@ -447,7 +447,7 @@ let purge_hyps_tac ~count =
           (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
-   let (_, metasenv, _, _, _) = proof in
+   let (_, metasenv, _subst, _, _, _) = proof in
     let (_, context, _) = CicUtil.lookup_meta goal metasenv in
      let proof',goal' = aux count context status in
       assert (goal = goal') ;
index 1e650cc7a047ca08e2d336c6300bb5ba2b652982..7d0e958cc40ce059e980a1b3d3a467eb2633756a 100644 (file)
@@ -1816,7 +1816,7 @@ let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) =
 
 let setoid_reflexivity_tac =
  let tac ((proof,goal) as status) =
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
    try
     let relation_class =
index 4e3badea4781e97f3595235971590e21eddae451..37800187ad4d290fb5c3bba38b9f53b78355c6b6 100644 (file)
@@ -52,11 +52,12 @@ class ['a] status
       incr next_id;
       !next_id
   in
-  let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ, attrs) in
+  let _subst = ([] : Cic.substitution) in
+  let initial_proof = ((uri: UriManager.uri option), metasenv, _subst, body, typ, attrs) in
   let next_goal (goals, proof) =
     match goals, proof with
     | goal :: _, _ -> Some goal
-    | [], (_, (goal, _, _) :: _, _, _, _) ->
+    | [], (_, (goal, _, _) :: _, _, _, _, _) ->
         (* the tactic left no open goal: let's choose the first open goal *)
         Some goal
     | _, _ -> None
@@ -109,24 +110,24 @@ class ['a] status
         raise exn
 *)
 
-    method uri      = let (uri, _, _, _, _)      = _proof in uri
-    method metasenv = let (_, metasenv, _, _, _) = _proof in metasenv
-    method body     = let (_, _, body, _, _)     = _proof in body
-    method typ      = let (_, _, _, typ, _)      = _proof in typ
-    method attrs    = let (_, _, _, _, attrs)    = _proof in attrs
+    method uri      = let (uri, _, _, _, _, _)      = _proof in uri
+    method metasenv = let (_, metasenv, _, _, _, _) = _proof in metasenv
+    method body     = let (_, _, _, body, _, _)     = _proof in body
+    method typ      = let (_, _, _, _, typ, _)      = _proof in typ
+    method attrs    = let (_, _, _, _, _, attrs)    = _proof in attrs
 
     method set_metasenv metasenv =
-      let (uri, _, body, typ, attes) = _proof in
-      _proof <- (uri, metasenv, body, typ, attrs)
+      let (uri, _,  _subst,body, typ, attes) = _proof in
+      _proof <- (uri, metasenv,  _subst,body, typ, attrs)
 
     method set_uri uri =
-      let (old_uri, metasenv, body, typ, attrs) = _proof in
+      let (old_uri, metasenv,  _subst,body, typ, attrs) = _proof in
       if old_uri <> None then
         raise Uri_redefinition;
-      _proof <- (Some uri, metasenv, body, typ, attrs)
+      _proof <- (Some uri, metasenv,  _subst,body, typ, attrs)
 
     method conjecture goal =
-      let (_, metasenv, _, _, _) = _proof in
+      let (_, metasenv, _subst, _, _, _) = _proof in
       CicUtil.lookup_meta goal metasenv
 
     method apply_tactic tactic =
index cc107451ee70182c1bbabbb4b8f557534bb87ef7..feff68f3fb8186f4ab4644ff2b07cce1b0e7accc 100644 (file)
@@ -40,7 +40,7 @@ module TC   = CicTypeChecker
 let lift_rewrite_tac ~context ~direction ~pattern equality =
    let lift_rewrite_tac status =
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
       let n = List.length new_context - List.length context in
       let equality = S.lift n equality in
@@ -51,7 +51,7 @@ let lift_rewrite_tac ~context ~direction ~pattern equality =
 let lift_destruct_tac ~context ~what =
    let lift_destruct_tac status =
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
       let n = List.length new_context - List.length context in
       let what = S.lift n what in
@@ -79,7 +79,7 @@ let rec subst_tac ~try_tactic ~hyp =
    in
    let subst_tac status =
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let what = match PEH.get_rel context hyp with
          | Some t -> t
@@ -148,7 +148,7 @@ let subst_tac =
          | _                  -> None
       in
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let tactics = HEL.list_rev_map_filter map context in
       let result = PET.apply_tactic (T.seq ~tactics) status in
index 3e9c1db2cbb59f2db82f313b5b934f6058ea8657..f3f7793032365bb5194137002b9356e0a2a80881 100644 (file)
@@ -42,7 +42,7 @@ module PET = ProofEngineTypes
 
 let id_tac = 
  let id_tac (proof,goal) = 
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _subst, _, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
   (proof,[goal])
  in 
@@ -50,7 +50,7 @@ let id_tac =
 
 let fail_tac =
  let fail_tac (proof,goal) =
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _subst, _ , _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
    raise (PET.Fail (lazy "fail tactical"))
  in
@@ -255,8 +255,8 @@ let solve_tactics ~tactics =
 
 let progress_tactic ~tactic =
   let msg = lazy "Failed to progress" in
-  let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
-    let ((_,metasenv',_,_,_),_) as ostatus =
+  let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
+    let ((_,metasenv',_subst,_,_,_),_) as ostatus =
      PET.apply_tactic tactic istatus
     in
      (*CSC: Warning
index 16a9c2267779cb27bb00866bdbf4751f70f0bb7a..3a3db7db43c4cf8cd1c0079b35ce6969ef89b24f 100644 (file)
@@ -38,7 +38,7 @@ let assumption_tac =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module PT = PrimitiveTactics in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
       hd::tl -> 
@@ -83,7 +83,7 @@ let generalize_tac
    let module C = Cic in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
-    let uri,metasenv,pbo,pty, attrs = proof in
+    let uri,metasenv,_subst,pbo,pty, attrs = proof in
     let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
     let subst,metasenv,u,selected_hyps,terms_with_context =
      ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
@@ -157,7 +157,7 @@ let generalize_tac
          else
           u1
       ) u terms_with_context) ;
-    let status = (uri,metasenv',pbo,pty, attrs),goal in
+    let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
     let proof,goals =
      PET.apply_tactic 
       (T.thens 
@@ -177,7 +177,7 @@ let generalize_tac
             T.id_tac])
         status
     in
-     let _,metasenv'',_,_, _ = proof in
+     let _,metasenv'',_subst,_,_, _ = proof in
       (* CSC: the following is just a bad approximation since a meta
          can be closed and then re-opened! *)
       (proof,
index 5df8656cdbb4cdbdffb930971c2ea4a0b19210ff..5873b22514e252da8579d6a890150ce9c8eb46ec 100644 (file)
@@ -167,8 +167,8 @@ let _ =
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with
             | GrafiteTypes.No_proof -> (Cic.Implicit None)
-            | Incomplete_proof i -> let _,_,p,_, _ = i.GrafiteTypes.proof in p
-            | Proof p -> let _,_,p,_, _ = p in p
+            | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,_subst,p,_, _ = p in p
             | Intermediate _ -> assert false)));
      addDebugItem "Print current proof (natural language) to stderr" 
        (fun _ -> 
@@ -179,9 +179,9 @@ let _ =
             with
             | GrafiteTypes.No_proof -> assert false
             | Incomplete_proof i -> 
-                let _,m,p,ty, attrs = i.GrafiteTypes.proof in 
+                let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in 
                 Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
-            | Proof (_,m,p,ty, attrs) -> 
+            | Proof (_,m,_subst,p,ty, attrs) -> 
                 Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
             | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
index 3b4c566e2a9a42c50c80bf7011cf37eabe0831a2..8d66ff56d1f80cd2d872c606c25486abfeb78c6b 100644 (file)
@@ -650,7 +650,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal None
 
-    method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
+    method load_sequents 
+      { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
+    =
       _metasenv <- metasenv;
       pages <- 0;
       let win goal_switch =
@@ -1092,11 +1094,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
-      | Proof  (uri, metasenv, bo, ty, attrs) ->
+      | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
-      | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
+      | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
index 9eb1dbf69c608c9ba231d4e46f45f3ae78fb1f18..fe8e691204800fb82d09cc5e3820a1896eae3361 100644 (file)
@@ -226,7 +226,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], "", parsed_text_length
   | TA.WHint (loc, term) ->
-     let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in
+     let _subst = [] in
+     let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in
      let l = List.map fst (MQ.experimental_hint ~dbd s) in
      let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
index aea67623e5809c90938dcc0112a01b409d11bfe5..b8eb18b4694b020399896a26a6f7ff23cf56376c 100644 (file)
@@ -155,7 +155,7 @@ let rec interactive_loop () =
         let watch_statuses lexicon_status grafite_status =
          match grafite_status.GrafiteTypes.proof_status with
             GrafiteTypes.Incomplete_proof
-             {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
+             {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
               GrafiteTypes.stack = stack } ->
               let open_goals = Continuationals.Stack.open_goals stack in
               print_endline