From 2e2648a9ed26d9b813de8e6a10e2776162565f09 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Apr 2008 19:18:53 +0000 Subject: [PATCH] oblivion ugraph everywhere outside the kernel --- .../components/acic_content/acic2content.ml | 6 ++--- .../acic_content/termAcicContent.ml | 2 +- .../acic_procedural/acic2Procedural.ml | 4 +-- .../acic_procedural/proceduralConversion.ml | 2 +- .../acic_procedural/proceduralHelpers.ml | 6 ++--- .../acic_procedural/proceduralOptimizer.ml | 2 +- helm/software/components/cic_acic/cic2acic.ml | 4 +-- .../cic_acic/doubleTypeInference.ml | 16 +++++------ .../components/cic_acic/eta_fixing.ml | 8 +++--- .../cic_disambiguation/disambiguate.ml | 14 +++++----- .../cic_exportation/cicExportation.ml | 8 +++--- .../components/cic_unification/cicRefine.ml | 4 +-- .../components/cic_unification/coercGraph.ml | 6 ++--- .../grafite_engine/grafiteEngine.ml | 4 +-- .../components/grafite_engine/grafiteSync.ml | 4 +-- .../components/lexicon/lexiconSync.ml | 2 +- helm/software/components/library/cicElim.ml | 5 ++-- helm/software/components/library/cicRecord.ml | 2 +- .../components/library/librarySync.ml | 8 +++--- .../metadata/metadataConstraints.ml | 2 +- .../components/metadata/metadataExtractor.ml | 6 ++--- helm/software/components/tactics/auto.ml | 27 ++++++++++--------- .../components/tactics/closeCoercionGraph.ml | 2 +- .../components/tactics/declarative.ml | 2 +- .../components/tactics/destructTactic.ml | 24 ++++++++--------- .../components/tactics/eliminationTactics.ml | 4 +-- .../components/tactics/equalityTactics.ml | 8 +++--- .../components/tactics/fwdSimplTactic.ml | 2 +- helm/software/components/tactics/inversion.ml | 14 +++++----- .../components/tactics/inversion_principle.ml | 2 +- .../components/tactics/metadataQuery.ml | 25 ++++++++--------- .../components/tactics/negationTactics.ml | 2 +- .../components/tactics/primitiveTactics.ml | 22 +++++++-------- .../tactics/proofEngineReduction.ml | 12 ++++----- .../tactics/proofEngineStructuralRules.ml | 12 ++++----- .../components/tactics/reductionTactics.ml | 4 +-- helm/software/components/tactics/ring.ml | 5 ++-- helm/software/components/tactics/setoids.ml | 11 +++++--- .../components/tactics/tacticChaser.ml | 2 +- helm/software/components/tactics/universe.ml | 2 +- .../components/tactics/variousTactics.ml | 6 ++--- 41 files changed, 155 insertions(+), 148 deletions(-) diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index b10464bda..b1423c5ab 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -427,7 +427,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_ if sort = `Prop then let inductive_types = (let o,_ = - CicEnvironment.get_obj CicUniv.empty_ugraph uri + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with | Cic.InductiveDefinition (l,_,_,_) -> l @@ -612,7 +612,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let inductive_types,noparams = - (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false @@ -780,7 +780,7 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner let ind_str = (prefix ^ ".ind") in let ind_uri = UriManager.uri_of_string ind_str in let inductive_types,noparams = - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in + (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in match o with | Cic.InductiveDefinition (l,_,n,_) -> (l,n) | _ -> assert false diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index f3806beea..2ce47bb67 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -42,7 +42,7 @@ type term_info = } let get_types uri = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno | _ -> assert false diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index c004fd346..e71f443d9 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -153,7 +153,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort" *) let get_type msg st bo = try - let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in + let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in ty with e -> failwith (msg ^ ": " ^ Printexc.to_string e) @@ -167,7 +167,7 @@ let get_entry st id = let get_ind_names uri tno = try - let ts = match E.get_obj Un.empty_ugraph uri with + let ts = match E.get_obj Un.oblivion_ugraph uri with | C.InductiveDefinition (ts, _, _, _), _ -> ts | _ -> assert false in diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 324141af4..30a52c32c 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -240,7 +240,7 @@ let clear c hyp = aux [] c let elim_inferred_type context goal arg using cpattern = - let metasenv, ugraph = [], Un.empty_ugraph in + let metasenv, ugraph = [], Un.oblivion_ugraph in let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in let _splits, args_no = PEH.split_with_whd (context, ety) in let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 31c7f4e8d..d599bdeb2 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -81,7 +81,7 @@ let compose f g x = f (g x) let fst3 (x, _, _) = x let refine c t = - try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t + try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t with e -> Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e); Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c); @@ -89,7 +89,7 @@ let refine c t = raise e let get_type c t = - try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty + try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty with e -> Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c); Printf.eprintf "TC: term : %s\n" (Pp.ppterm t); @@ -124,7 +124,7 @@ let is_not_atomic = function let is_atomic t = not (is_not_atomic t) let get_ind_type uri tyno = - match E.get_obj Un.empty_ugraph uri with + match E.get_obj Un.oblivion_ugraph uri with | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno | _ -> assert false diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 776d52645..e16828fa7 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -42,7 +42,7 @@ let defined_premise = "DEFINED" let get_type msg c bo = try - let ty, _ = TC.type_of_aux' [] c bo Un.empty_ugraph in + let ty, _ = TC.type_of_aux' [] c bo Un.oblivion_ugraph in ty with e -> failwith (msg ^ ": " ^ Printexc.to_string e) diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index c5bbfff78..c2f1616be 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -49,11 +49,11 @@ let xxx_add h k v = let xxx_type_of_aux' m c t = let res,_ = try - CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph with | CicTypeChecker.AssertFailure _ | CicTypeChecker.TypeCheckerFailure _ -> - Cic.Sort Cic.Prop, CicUniv.empty_ugraph + Cic.Sort Cic.Prop, CicUniv.oblivion_ugraph in res ;; diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index d54d0fbe4..6fa7cce5a 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -37,7 +37,7 @@ exception RelToHiddenHypothesis;; let xxx_type_of_aux' m c t = try - Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph)) + Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph)) with | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *) ;; @@ -180,7 +180,7 @@ let type_of_constant uri = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj (uobj,_) -> raise (NotWellTyped "Reference to an unchecked constant") @@ -195,7 +195,7 @@ let type_of_variable uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty | CicEnvironment.UncheckedObj (C.Variable _,_) -> raise (NotWellTyped "Reference to an unchecked variable") @@ -207,7 +207,7 @@ let type_of_mutual_inductive_defs uri i = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj (uobj,_) -> raise (NotWellTyped "Reference to an unchecked inductive type") @@ -224,7 +224,7 @@ let type_of_mutual_inductive_constr uri i j = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj (uobj,_) -> raise (NotWellTyped "Reference to an unchecked constructor") @@ -464,7 +464,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (cl,parsno) = let obj,_ = try - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri with Not_found -> assert false in match obj with @@ -573,7 +573,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let uris_and_types = let obj,_ = try - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri with Not_found -> assert false in let params = CicUtil.params_of_obj obj in @@ -581,7 +581,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (function uri -> let obj,_ = try - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri with Not_found -> assert false in match obj with diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml index 90f33d081..9ebd48b8b 100644 --- a/helm/software/components/cic_acic/eta_fixing.ml +++ b/helm/software/components/cic_acic/eta_fixing.ml @@ -211,7 +211,7 @@ let eta_fix metasenv context t = let tl' = List.map (eta_fix' context) tl in let ty,_ = CicTypeChecker.type_of_aux' metasenv context he - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in fix_according_to_type ty (eta_fix' context he) tl' (* @@ -240,7 +240,7 @@ let eta_fix metasenv context t = let term' = eta_fix' context term in let patterns' = List.map (eta_fix' context) patterns in let inductive_types,noparams = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in (match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false @@ -261,7 +261,7 @@ let eta_fix metasenv context t = else let term_type,_ = CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in (match term_type with C.Appl (hd::params) -> @@ -300,7 +300,7 @@ let eta_fix metasenv context t = (fun newsubst (uri,t) -> let t' = eta_fix' context t in let ty = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with Cic.Variable (_,_,ty,_,_) -> CicSubstitution.subst_vars newsubst ty diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index d58dc9854..ad8028d16 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -255,7 +255,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\"")) ) branches else - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with Cic.InductiveDefinition (il,_,leftsno,_) -> let _,_,_,cl = try @@ -484,16 +484,16 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ (try match cic with | Cic.Const (uri, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.Const (uri, mk_subst uris) | Cic.Var (uri, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.Var (uri, mk_subst uris) | Cic.MutInd (uri, i, []) -> (try - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.MutInd (uri, i, mk_subst uris) with @@ -506,7 +506,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ (*here the explicit_named_substituion is assumed to be of length 0 *) Cic.MutInd (uri,i,[])) | Cic.MutConstruct (uri, i, j, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.MutConstruct (uri, i, j, mk_subst uris) | Cic.Meta _ | Cic.Implicit _ as t -> @@ -976,7 +976,7 @@ module Make (C: Callbacks) = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe + ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing (thing_txt,thing_txt_prefix_len,thing) = @@ -1276,7 +1276,7 @@ in refine_profiler.HExtlib.profile foo () failwith "Disambiguate: circular dependency" let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe + ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe (text,prefix_len,term) = let term = diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 69c949c63..cd5ab3ace 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -223,7 +223,7 @@ let rec pp ~in_type t context = (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) -> let nparams = - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (_,_,nparams,_) -> nparams | _ -> assert false in let hes = pp ~in_type he context in @@ -236,7 +236,7 @@ let rec pp ~in_type t context = pp_exp_named_subst exp_named_subst context | C.MutInd (uri,n,exp_named_subst) -> (try - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (dl,_,_,_) -> let (name,_,_,_) = get_nth dl (n+1) in qualified_name_of_uri current_module_uri @@ -250,7 +250,7 @@ let rec pp ~in_type t context = ) | C.MutConstruct (uri,n1,n2,exp_named_subst) -> (try - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (dl,_,_,_) -> let _,_,_,cons = get_nth dl (n1+1) in let id,_ = get_nth cons n2 in @@ -289,7 +289,7 @@ let rec pp ~in_type t context = if patterns = [] then "assert false" else (let connames_and_argsno, go_up, go_pu, go_down, go_nwod = - (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (dl,_,paramsno,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in let rc = diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 065dbc33d..5aa96944d 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -649,7 +649,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (let candidate,ugraph5,metasenv,subst = let exp_name_subst, metasenv = let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in List.fold_right ( @@ -1847,7 +1847,7 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno = metasenv,ugraph,substituted_tys let typecheck metasenv uri obj ~localization_tbl = - let ugraph = CicUniv.empty_ugraph in + let ugraph = CicUniv.oblivion_ugraph in match obj with Cic.Constant (name,Some bo,ty,args,attrs) -> (* CSC: ugly code. Here I need to retrieve in advance the loc of bo diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index f12ea14b1..ac7441a4c 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -52,7 +52,7 @@ let saturate_coercion ul metasenv subst context = (fun arity (c,saturations) -> let ty,_ = CicTypeChecker.type_of_aux' ~subst metasenv context c - CicUniv.empty_ugraph in + CicUniv.oblivion_ugraph in let _,metasenv,args,lastmeta = TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in let irl = @@ -158,7 +158,7 @@ let is_composite t = | Cic.Appl (he::_) -> CicUtil.uri_of_term he | _ -> CicUtil.uri_of_term t in - match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with | Cic.Constant (_,_, _, _, attrs),_ -> List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs | _ -> false @@ -182,7 +182,7 @@ let coerced_arg l = | _ -> 0 in let uri = CicUtil.uri_of_term c in - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with | Cic.Constant (_, _, ty, _, _) -> count_pi ty | _ -> assert false in diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index bc56ce35d..a73e53a1f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -557,7 +557,7 @@ let add_coercions_of_record_to_moo obj lemmas status = let is_a_coercion uri = try let obj,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in let attrs = CicUtil.attributes_of_obj obj in try match List.find @@ -746,7 +746,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let t = CicUtil.term_of_uri u in let ty',g = CicTypeChecker.type_of_aux' - metasenv' [] t CicUniv.empty_ugraph + metasenv' [] t CicUniv.oblivion_ugraph in fst(CicReduction.are_convertible [] ty' ty g)) similar diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index d318d11a7..b6b9f7e5a 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -58,9 +58,9 @@ let add_obj refinement_toolkit uri obj status = let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in let add_to_universe (universe,status) uri = let term = CicUtil.term_of_uri uri in - let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in + let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in (* prop filtering - let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in + let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.oblivion_ugraph in prerr_endline (CicPp.ppterm term); prerr_endline (CicPp.ppterm sort); let tkeys = diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml index 30031943d..9010dfcff 100644 --- a/helm/software/components/lexicon/lexiconSync.ml +++ b/helm/software/components/lexicon/lexiconSync.ml @@ -83,7 +83,7 @@ let add_aliases_for_object status uri = let add_aliases_for_objs = List.fold_left (fun status uri -> - let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in add_aliases_for_object status uri obj) module OrderedId = diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml index 3cb5ee4e8..aacace7b5 100644 --- a/helm/software/components/library/cicElim.ml +++ b/helm/software/components/library/cicElim.ml @@ -259,7 +259,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args = let elim_of ~sort uri typeno = counter := ~-1; - let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in + let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in match obj with | Cic.InductiveDefinition (indTypes, params, leftno, _) -> let (name, inductive, ty, constructors) = @@ -394,7 +394,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body)); *) let (computed_type, ugraph) = try - CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' [] [] eliminator_body + CicUniv.oblivion_ugraph with CicTypeChecker.TypeCheckerFailure msg -> raise (Elim_failure (lazy (sprintf "type checker failure while type checking:\n%s\nerror:\n%s" diff --git a/helm/software/components/library/cicRecord.ml b/helm/software/components/library/cicRecord.ml index 775292ccb..5502f989e 100644 --- a/helm/software/components/library/cicRecord.ml +++ b/helm/software/components/library/cicRecord.ml @@ -43,7 +43,7 @@ let generate_one_proj uri params paramsno fields t i = let projections_of uri field_names = let buri = UriManager.buri_of_uri uri in - let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in + let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in match obj with Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) -> assert (params = []); (* general case not implemented *) diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 8a0c2bcc4..fd89f77c8 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -229,7 +229,7 @@ let generate_elimination_principles uri refinement_toolkit = List.iter remove_single_obj !uris; raise exn in - let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in + let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in match obj with | Cic.InductiveDefinition (indTypes, _, _, _) -> let counter = ref 0 in @@ -273,7 +273,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in - CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph in (* we have to get the source and the tgt type uri * in Coq syntax we have already their names, but @@ -420,8 +420,8 @@ let generate_projections refinement_toolkit uri fields = (fun (uri, name, bo) (_name, coercion, arity) -> let saturations = 0 in try - let ty, ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let ty, _ = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in add_single_obj uri obj refinement_toolkit; diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml index ccd88f104..3e8ac2f72 100644 --- a/helm/software/components/metadata/metadataConstraints.ml +++ b/helm/software/components/metadata/metadataConstraints.ml @@ -385,7 +385,7 @@ and signature_concl = List.flatten (List.map (fun uri -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in projections_of (CicUtil.projections_of_record o uri)) uris) in diff --git a/helm/software/components/metadata/metadataExtractor.ml b/helm/software/components/metadata/metadataExtractor.ml index 462679534..63db2331d 100644 --- a/helm/software/components/metadata/metadataExtractor.ml +++ b/helm/software/components/metadata/metadataExtractor.ml @@ -70,7 +70,7 @@ let incr_depth = function | _ -> assert false let var_has_body uri = - match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with | Cic.Variable (_, Some body, _, _, _), _ -> true | _ -> false @@ -287,7 +287,7 @@ let depth_offset params = List.length (List.filter (non var_has_body) params) let rec compute_var pos uri = - let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with | Cic.Variable (_, Some _, _, _, _) -> S.empty | Cic.Variable (_, None, ty, params, _) -> @@ -310,7 +310,7 @@ let rec compute_var pos uri = | _ -> assert false let compute_obj uri = - let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with | Cic.Variable (_, body, ty, params, _) | Cic.Constant (_, body, ty, params, _) -> diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 41ea1e5e4..fabfcf4de 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -90,7 +90,7 @@ let find_library_theorems dbd proof goal = let terms = List.map CicUtil.term_of_uri univ in List.map (fun t -> - (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph))) + (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph))) terms let find_context_theorems context metasenv = @@ -131,7 +131,7 @@ let is_unit_equation context metasenv oldnewmeta term = let _,_,mt = CicUtil.lookup_meta i metasenv in let sort,u = CicTypeChecker.type_of_aux' metasenv context mt - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in let b, _ = CicReduction.are_convertible ~metasenv context @@ -163,7 +163,7 @@ let get_candidates universe cache t = let only signature context metasenv t = try let ty,_ = - CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph in let consts = MetadataConstraints.constants_of ty in let b = MetadataConstraints.UriManagerSet.subset consts signature in @@ -268,7 +268,7 @@ let init_cache_and_tables (fun t -> let ty,_ = CicTypeChecker.type_of_aux' - metasenv context t CicUniv.empty_ugraph + metasenv context t CicUniv.oblivion_ugraph in (* retrieve_equations could also return flexible terms *) if is_an_equality ty then Some(t,ty) @@ -285,7 +285,7 @@ let init_cache_and_tables in (* SIMPLIFICATION STEP let equalities = - let env = (metasenv, context, CicUniv.empty_ugraph) in + let env = (metasenv, context, CicUniv.oblivion_ugraph) in let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in Saturation.simplify_equalities bag eq_uri env units in @@ -312,7 +312,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u let _,_,mt = CicUtil.lookup_meta i metasenv in let sort,u = CicTypeChecker.type_of_aux' metasenv context mt - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in let b, _ = CicReduction.are_convertible ~metasenv context @@ -401,7 +401,8 @@ let close_more tables maxmeta context status auto universe cache = HExtlib.filter_map (fun t -> let ty,_ = - CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.oblivion_ugraph in (* retrieve_equations could also return flexible terms *) if is_an_equality ty then Some(t,ty) else None) equations in @@ -663,7 +664,7 @@ let apply_smart in let metasenv' = metasenv@newmetasenvfragment in let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph in let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in let goal_arity = count_prods context ty in @@ -677,21 +678,21 @@ let apply_smart (****************** AUTO ********************) let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;; -let ugraph = CicUniv.empty_ugraph;; +let ugraph = CicUniv.oblivion_ugraph;; let typeof = CicTypeChecker.type_of_aux';; let ppterm ctx t = let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in CicPp.pp t names ;; let is_in_prop context subst metasenv ty = - let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in + let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u) ;; let assert_proof_is_valid proof metasenv context goalty = if debug then begin - let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in + let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in let b,_ = CicReduction.are_convertible context ty goalty u in if not b then begin @@ -1636,7 +1637,7 @@ let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= (* we demodulate using both actives passives *) List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities in - let env = metasenv,context,CicUniv.empty_ugraph in + let env = metasenv,context,CicUniv.oblivion_ugraph in match Indexing.solve_demodulating bag env table initgoal steps with | Some (proof, metasenv, newty) -> let refl = @@ -1681,7 +1682,7 @@ let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= in let changed,(newproof,newmetasenv, newty) = Indexing.demodulation_goal bag - (metasenv,context,CicUniv.empty_ugraph) table initgoal + (metasenv,context,CicUniv.oblivion_ugraph) table initgoal in if changed then begin diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 7ed3c36e6..e9a123ad8 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -461,7 +461,7 @@ let close_coercion_graph src tgt uri saturations baseuri = let o,univ = build_obj t univ arityres in (o,saturationsres,arityres),univ | _ -> assert false - ) (first_step, CicUniv.empty_ugraph) tl + ) (first_step, CicUniv.oblivion_ugraph) tl in let name_src = CoercDb.name_of_carr src in let name_tgt = CoercDb.name_of_carr tgt in diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index db1345344..b9c0779c7 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -170,7 +170,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[]) in let ty,_ = - CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in let just' = match just with `Auto (univ, params) -> diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml index a8bfc007d..f6fb61ac1 100644 --- a/helm/software/components/tactics/destructTactic.ml +++ b/helm/software/components/tactics/destructTactic.ml @@ -92,7 +92,7 @@ let discriminate_tac ~term = let mk_branches_and_outtype turi typeno consno context args = (* a list of "True" except for the element in position consno which * is "False" *) - match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with + match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with | C.InductiveDefinition (ind_type_list,_,paramsno,_) -> let _,_,rty,constructor_list = List.nth ind_type_list typeno in let false_constr_id,_ = List.nth constructor_list (consno - 1) in @@ -158,7 +158,7 @@ let discriminate_tac ~term = let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = - CTC.type_of_aux' metasenv context term CU.empty_ugraph + CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] @@ -226,7 +226,7 @@ let clear_term first_time lterm = let (proof, goal) = status in let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in debug_print (lazy ("\nclear di: " ^ pp context term)); debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); let g () = if first_time then raise exn_nothingtodo else T.id_tac in @@ -277,9 +277,9 @@ let injection_tac ~lterm ~i ~continuation ~recur = * del costruttore *) let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in let termty,_ = - CTC.type_of_aux' metasenv context term CU.empty_ugraph + CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in debug_print (lazy ("\ninjection su : " ^ pp context termty)); match termty with (* an equality *) @@ -301,9 +301,9 @@ let injection_tac ~lterm ~i ~continuation ~recur = List.nth applist1 (pred i),List.nth applist2 (pred i),consno2 | _ -> assert false in - let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in + let tty',_ = CTC.type_of_aux' metasenv context t1' CU.oblivion_ugraph in let patterns,outtype = - match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with + match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with | C.InductiveDefinition (ind_type_list,_,paramsno,_)-> let left_params, right_params = HExtlib.split_nth paramsno params in let _,_,_,constructor_list = List.nth ind_type_list typeno in @@ -383,7 +383,7 @@ let injection_tac ~lterm ~i ~continuation ~recur = let go_on = try let _,g = CTC.type_of_aux' metasenv context cutted - CU.empty_ugraph + CU.oblivion_ugraph in let _,g = CTC.type_of_aux' metasenv context changed g in fst (CR.are_convertible ~metasenv context t1' changed g) @@ -442,7 +442,7 @@ let subst_tac ~lterm ~direction ~where ~continuation ~recur = let (proof, goal) = status in let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term)); let tactic = match where with | None -> @@ -463,18 +463,18 @@ let subst_tac ~lterm ~direction ~where ~continuation ~recur = let rec destruct ~first_time lterm = let are_convertible hd1 hd2 metasenv context = - fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph) + fst (CR.are_convertible ~metasenv context hd1 hd2 CU.oblivion_ugraph) in let recur = destruct ~first_time:false in let destruct status = let (proof, goal) = status in let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in + let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in let tactic = if not (first_time || exists context term) then T.id_tac else begin debug_print (lazy ("\ndestruct di: " ^ pp context term)); debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); - let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in + let termty,_ = CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in debug_print (lazy ("\ndestruct su: " ^ pp context termty)); let mk_lterm term c m ug = let distance = List.length c - List.length context in diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index 29961db38..6e0c223d2 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -43,7 +43,7 @@ module PEH = ProofEngineHelpers let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None let get_inductive_def uri = - match E.get_obj Un.empty_ugraph uri with + match E.get_obj Un.oblivion_ugraph uri with | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, tys | _ -> assert false @@ -70,7 +70,7 @@ let rec check_type sorts metasenv context t = let _, psno = PEH.split_with_whd ([], arity) in let not_relation = (lpsno = psno) in let not_recursive = is_not_recursive uri tyno tys in - let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in + let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in let sort = match PEH.split_with_whd (context, ty_ty) with | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort | (_, C.Meta _) :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ())) diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 72a63571c..47f422f52 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -104,7 +104,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in let ty_eq,ugraph = CicTypeChecker.type_of_aux' metasenv context equality - CicUniv.empty_ugraph in + CicUniv.oblivion_ugraph in let (ty_eq,metasenv',arguments,fresh_meta) = TermUtil.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in @@ -241,7 +241,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = in let context_len = List.length context in let subst,metasenv,u,_,selected_terms_with_context = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let with_what, metasenv, u = with_what context metasenv u in @@ -251,7 +251,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = 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 + metasenv context with_what CicUniv.oblivion_ugraph in let whats = match selected_terms_with_context with [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected")) @@ -278,7 +278,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = (lazy "Replace: one of the selected terms is not closed")) in let ty_of_t_in_context,u = (* TASSI: FIXME *) CicTypeChecker.type_of_aux' metasenv context t_in_context - CicUniv.empty_ugraph in + CicUniv.oblivion_ugraph in let b,u = CicReduction.are_convertible ~metasenv context ty_of_with_what ty_of_t_in_context u in if b then diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml index 8734837d1..10df83c5d 100644 --- a/helm/software/components/tactics/fwdSimplTactic.ml +++ b/helm/software/components/tactics/fwdSimplTactic.ml @@ -111,7 +111,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name let lapply_tac (proof, goal) = 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, _ = TC.type_of_aux' metasenv context what U.oblivion_ugraph in let lemma = FNG.clean_dummy_dependent_types lemma in let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in let conclusion = diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml index e61021244..3b4000ea4 100644 --- a/helm/software/components/tactics/inversion.ml +++ b/helm/software/components/tactics/inversion.ml @@ -190,9 +190,9 @@ let private_inversion_tac ~term = | Some uri -> uri in let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in - let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in let uri = baseuri_of_term termty in - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let (_,_,typeno,_) = match termty with C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) @@ -215,7 +215,7 @@ let private_inversion_tac ~term = let parameters_tys = (List.map (fun t -> ( - match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with + match (T.type_of_aux' metasenv context t CicUniv.oblivion_ugraph) with (term,graph) -> term)) parameters) in @@ -261,7 +261,7 @@ let private_inversion_tac ~term = (*DEBUG*) debug_print (lazy ("private inversion: term before refinement: " ^ CicPp.ppterm t)); let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in (*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: " ^ CicPp.ppterm ref_t)); @@ -307,7 +307,7 @@ let inversion_tac ~term = (*DEBUG*) debug_print (lazy ("inversion begins")); 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 termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in let uri, typeno = match termty with | Cic.MutInd (uri,typeno,_) @@ -315,7 +315,7 @@ let inversion_tac ~term = | _ -> assert false in (* let uri = baseuri_of_term termty in *) - let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let name,nleft,arity,cons_list = match obj with Cic.InductiveDefinition (tys,_,nleft,_) -> @@ -342,7 +342,7 @@ let inversion_tac ~term = let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in let (t1,metasenv,_subst,t3,t4, attrs) = proof in let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in let proof = (t1,metasenv'',_subst,t3,t4, attrs) in let proof3,gl3 = diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index f2dd37f9e..2b6e14b37 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -145,7 +145,7 @@ let build_inversion uri obj = debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem - CicUniv.empty_ugraph in + CicUniv.oblivion_ugraph in (*DEBUG*) debug_print (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); let buri = UriManager.buri_of_uri uri in diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index 2941a806e..571a045ad 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -51,11 +51,11 @@ let signature_of_hypothesis context metasenv = try let ty,_ = CicTypeChecker.type_of_aux' - metasenv current_ctx t CicUniv.empty_ugraph + metasenv current_ctx t CicUniv.oblivion_ugraph in let sort,_ = CicTypeChecker.type_of_aux' - metasenv current_ctx ty CicUniv.empty_ugraph + metasenv current_ctx ty CicUniv.oblivion_ugraph in let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in match sort with @@ -113,15 +113,15 @@ let compare_goal_list proof goal1 goal2 = 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 CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in let ty_sort2,_ = - CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph in let prop1 = let b,_ = CicReduction.are_convertible - ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph + ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph in if b then 0 else 1 @@ -129,7 +129,7 @@ let compare_goal_list proof goal1 goal2 = let prop2 = let b,_ = CicReduction.are_convertible - ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph + ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph in if b then 0 else 1 @@ -150,7 +150,7 @@ let close_with_types s metasenv context = (fun e bag -> let t = CicUtil.term_of_uri e in let ty, _ = - CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph in Constr.UriManagerSet.union bag (Constr.constants_of ty)) s s @@ -162,7 +162,7 @@ let close_with_constructors s metasenv context = match t with Cic.MutInd (uri,_,_) | Cic.MutConstruct (uri,_,_,_) -> - (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with Cic.InductiveDefinition(tl,_,_,_) -> snd (List.fold_left @@ -215,7 +215,7 @@ let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) = let is_predicate u = let ty, _ = try CicTypeChecker.type_of_aux' [] [] - (CicUtil.term_of_uri u) CicUniv.empty_ugraph + (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph with CicTypeChecker.TypeCheckerFailure _ -> assert false in let rec check_last_pi = function @@ -229,7 +229,7 @@ let is_predicate u = let only constants uri = prerr_endline (UriManager.string_of_uri uri); let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *) - let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in let consts = Constr.constants_of ty in (* prerr_endline ("XXX " ^ UriManager.string_of_uri uri); @@ -260,7 +260,7 @@ let types_for_equality metasenv goal = (fun (i,acc) _ -> let ty, _ = CicTypeChecker.type_of_aux' - metasenv context (Cic.Rel i) CicUniv.empty_ugraph in + metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in let newty = types_of_equality ty in (i+1,Constr.SetSet.union newty acc)) (1,all) context @@ -424,7 +424,8 @@ let experimental_hint | Some (main,_) -> let ty, _ = CicTypeChecker.type_of_aux' - metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph + metasenv context (CicUtil.term_of_uri main) + CicUniv.oblivion_ugraph in Constr.constants_of ty in diff --git a/helm/software/components/tactics/negationTactics.ml b/helm/software/components/tactics/negationTactics.ml index fb904bf36..287ec4dfe 100644 --- a/helm/software/components/tactics/negationTactics.ml +++ b/helm/software/components/tactics/negationTactics.ml @@ -39,7 +39,7 @@ let absurd_tac ~term = | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command")) in let ty_term,_ = - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *) then ProofEngineTypes.apply_tactic (P.apply_tac diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index e7632ebf4..53bfc39a9 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -136,7 +136,7 @@ let eta_expand metasenv context t arg = List.map (function uri,t -> uri,aux n t) in let argty,_ = - T.type_of_aux' metasenv context arg CicUniv.empty_ugraph (* TASSI: FIXME *) + T.type_of_aux' metasenv context arg CicUniv.oblivion_ugraph (* TASSI: FIXME *) in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst:[] @@ -182,7 +182,7 @@ let = let module C = Cic in let params = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in CicUtil.params_of_obj o in let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'= @@ -194,7 +194,7 @@ let [],[] -> [] | uri::tl,[] -> let ty = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with C.Variable (_,_,ty,_,_) -> CicSubstitution.subst_vars !exp_named_subst_diff ty @@ -242,7 +242,7 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termt goal_arity in let subst,newmetasenv',_ = CicUnification.fo_unif_subst - subst context newmetasenv consthead ty CicUniv.empty_ugraph + subst context newmetasenv consthead ty CicUniv.oblivion_ugraph in let t = if List.length arguments = 0 then term' else Cic.Appl (term'::arguments) @@ -296,7 +296,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = in let metasenv' = metasenv@newmetasenvfragment in let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph in let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in @@ -436,7 +436,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: (ProofEngineTypes.Fail (lazy "You can't letin a term containing the current goal")); let tty,_ = - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in @@ -464,7 +464,7 @@ let exact_tac ~term = let metano,context,ty = CicUtil.lookup_meta goal metasenv in let module T = CicTypeChecker in let module R = CicReduction in - let ty_term,u = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *) if b then begin @@ -614,7 +614,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = | None, [], Some cpattern -> cpattern | _ -> raise (PET.Fail (lazy "not implemented")) in - let ugraph = CicUniv.empty_ugraph in + let ugraph = CicUniv.oblivion_ugraph in let curi, metasenv, _subst, proofbo, proofty, attrs = proof in let conjecture = CicUtil.lookup_meta goal metasenv in let metano, context, ty = conjecture in @@ -721,7 +721,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera let module C = Cic 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,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in let termty = CicReduction.whd context termty in let (termty,metasenv',arguments,fresh_meta) = TermUtil.saturate_term @@ -735,7 +735,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera | _ -> raise NotAnInductiveTypeToEliminate in let paramsno,itty,patterns,right_args = - match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with | C.InductiveDefinition (tys,_,paramsno,_),_ -> let _,left_parameters,right_args = List.fold_right @@ -824,7 +824,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in let refined_term,_,metasenv'',_ = CicRefine.type_of_aux' metasenv' context term_to_refine - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in let new_goals = ProofEngineHelpers.compare_metasenvs diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 3892ace35..d5dbf9f35 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -417,7 +417,7 @@ let unfold ?what context where = with Failure _ -> assert false) | Cic.Const (uri,exp_named_subst) as t -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in (match o with Cic.Constant (_,Some body,_,_,_) -> CicReduction.head_beta_reduce @@ -428,7 +428,7 @@ let unfold ?what context where = | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) | Cic.Var (uri,exp_named_subst) as t -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in (match o with Cic.Constant _ -> raise ReferenceToConstant | Cic.CurrentProof _ -> raise ReferenceToCurrentProof @@ -512,7 +512,7 @@ let simpl context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -553,7 +553,7 @@ let simpl context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with C.Constant (_,Some body,_,_,_) -> if List.exists is_active l then @@ -612,7 +612,7 @@ let simpl context = C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in match o with C.InductiveDefinition (tl,ingredients,r,_) -> let (_,_,arity,_) = List.nth tl i in @@ -870,7 +870,7 @@ let simpl context = prerr_endline (CicPp.ppterm t2 ^ "\n"); let subst1, _, _ = CicUnification.fo_unif metasenv ctx t1 t2 - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph in prerr_endline "UNIFICANO\n\n\n"; subst := subst1; diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index 3f96677b8..479219537 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.ml +++ b/helm/software/components/tactics/proofEngineStructuralRules.ml @@ -53,7 +53,7 @@ let clearbody ~hyp = let _,_ = try CicTypeChecker.type_of_aux' metasenv context t - CicUniv.empty_ugraph (* TASSI: FIXME *) + CicUniv.oblivion_ugraph (* TASSI: FIXME *) with _ -> raise @@ -68,10 +68,10 @@ let clearbody ~hyp = (try ignore (CicTypeChecker.type_of_aux' metasenv context te - CicUniv.empty_ugraph (* TASSI: FIXME *)); + CicUniv.oblivion_ugraph (* TASSI: FIXME *)); ignore (CicTypeChecker.type_of_aux' metasenv context ty - CicUniv.empty_ugraph (* TASSI: FIXME *)); + CicUniv.oblivion_ugraph (* TASSI: FIXME *)); with _ -> raise @@ -86,7 +86,7 @@ let clearbody ~hyp = let _,_ = try CicTypeChecker.type_of_aux' metasenv canonical_context' ty - CicUniv.empty_ugraph (* TASSI: FIXME *) + CicUniv.oblivion_ugraph (* TASSI: FIXME *) with _ -> raise @@ -130,7 +130,7 @@ let clear_one ~hyp = let _,_ = try CicTypeChecker.type_of_aux' metasenv context t - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph with _ -> raise (PET.Fail @@ -147,7 +147,7 @@ let clear_one ~hyp = let _,_ = try CicTypeChecker.type_of_aux' metasenv canonical_context' ty - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph with _ -> raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) in diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index 8a0d739be..c943e7a19 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -51,7 +51,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) = CicMetaSubst.apply_subst subst where', metasenv, ugraph in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in @@ -167,7 +167,7 @@ let change_tac ?(with_cast=false) ~pattern with_what = CicMetaSubst.apply_subst subst where', metasenv, ugraph in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in let context', metasenv, ugraph = diff --git a/helm/software/components/tactics/ring.ml b/helm/software/components/tactics/ring.ml index 7695a4ff0..82ef5f4f2 100644 --- a/helm/software/components/tactics/ring.ml +++ b/helm/software/components/tactics/ring.ml @@ -503,7 +503,7 @@ let ring_tac status = let status' = (* status after 1st elim_type use *) let context = context_of_status status in let b,_ = (*TASSI : FIXME*) - are_convertible context t1'' t1 CicUniv.empty_ugraph in + are_convertible context t1'' t1 CicUniv.oblivion_ugraph in if not b then begin warn (lazy "t1'' and t1 are NOT CONVERTIBLE"); let newstatus = @@ -544,7 +544,8 @@ let ring_tac status = let status' = let context = context_of_status status in let b,_ = (* TASSI:FIXME *) - are_convertible context t2'' t2 CicUniv.empty_ugraph + are_convertible context t2'' t2 + CicUniv.oblivion_ugraph in if not b then begin warn (lazy "t2'' and t2 are NOT CONVERTIBLE"); diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml index c8ca16317..d85df1c4b 100644 --- a/helm/software/components/tactics/setoids.ml +++ b/helm/software/components/tactics/setoids.ml @@ -646,18 +646,21 @@ let unify_relation_carrier_with_type env rel t = let argsno = List.length args' - rel.rel_quantifiers_no in let args1 = list_sub args' 0 argsno in let args2 = list_sub args' argsno rel.rel_quantifiers_no in - if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) CicUniv.empty_ugraph) then + if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) + CicUniv.oblivion_ugraph) then args2 else raise_error rel.rel_quantifiers_no | _ -> - if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then + if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] + rel.rel_a t CicUniv.oblivion_ugraph) then [] else begin (*COQ let evars,args,instantiated_rel_a = - let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in + let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a + CicUniv.oblivion_ugraph in let evd = Evd.create_evar_defs Evd.empty in let evars,args,concl = Clenv.clenv_environments_evars env evd @@ -682,7 +685,7 @@ let unify_relation_carrier_with_type env rel t = let unify_relation_class_carrier_with_type env rel t = match rel with Leibniz (Some t') -> - if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then + if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then rel else raise (ProofEngineTypes.Fail (lazy diff --git a/helm/software/components/tactics/tacticChaser.ml b/helm/software/components/tactics/tacticChaser.ml index cb700f776..f7ea9d9e3 100644 --- a/helm/software/components/tactics/tacticChaser.ml +++ b/helm/software/components/tactics/tacticChaser.ml @@ -237,7 +237,7 @@ let searchTheorems mqi_handle (proof,goal) = prerr_endline "PRIMA DELLA PRIMA TYPE OF " ; *) let ty_sort1,u = (*TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in (* prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2)); *) diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index c4e439efe..f7c3932dc 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -162,7 +162,7 @@ let remove univ context term ty = let remove_uri univ uri = let term = CicUtil.term_of_uri uri in - let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in + let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in remove univ [] term ty diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml index 5563f206b..28dc4575d 100644 --- a/helm/software/components/tactics/variousTactics.ml +++ b/helm/software/components/tactics/variousTactics.ml @@ -45,10 +45,10 @@ let assumption_tac = (match hd with (Some (_, C.Decl t)) when fst (R.are_convertible context (S.lift n t) ty - CicUniv.empty_ugraph) -> n + CicUniv.oblivion_ugraph) -> n | (Some (_, C.Def (_,ty'))) when fst (R.are_convertible context (S.lift n ty') ty - CicUniv.empty_ugraph) -> n + CicUniv.oblivion_ugraph) -> n | _ -> find (n+1) tl ) | [] -> raise (PET.Fail (lazy "Assumption: No such assumption")) @@ -80,7 +80,7 @@ let generalize_tac 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 + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let context = CicMetaSubst.apply_subst_context subst context in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in -- 2.39.2