diff options
Diffstat (limited to 'plugins')
47 files changed, 467 insertions, 355 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index da8955f0d7..a09abfa193 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -200,7 +200,8 @@ module Btauto = struct let assign = List.combine env var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let term = Printer.pr_constr key in + let sigma, env = Pfedit.get_current_context () in + let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in let assign = List.map map_msg assign in diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index faabd7c143..ccef9ab960 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -12,13 +12,13 @@ open CErrors open Pp -open Goptions open Names -open Term +open Sorts open Constr open Vars -open Tacmach open Evd +open Goptions +open Tacmach open Util let init_size=5 @@ -437,7 +437,7 @@ and make_app l=function and applist_proj c l = match c with | Symb s -> applist_projection s l - | _ -> applistc (constr_of_term c) l + | _ -> Term.applistc (constr_of_term c) l and applist_projection c l = match Constr.kind c with | Const c when Environ.is_projection (fst c) (Global.env()) -> @@ -447,10 +447,10 @@ and applist_projection c l = let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx + Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx | hd :: tl -> - applistc (mkProj (p, hd)) tl) - | _ -> applistc c l + Term.applistc (mkProj (p, hd)) tl) + | _ -> Term.applistc c l let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in @@ -838,7 +838,7 @@ let complete_one_class state i= let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in - let typ = prod_applist _c (List.rev _args) in + let typ = Term.prod_applist _c (List.rev _args) in let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7dec34d4d7..8642df6846 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -12,7 +12,6 @@ open Evd open Names open Inductiveops open Declarations -open Term open Constr open EConstr open Vars diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 47e8123191..4ae875cd70 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -302,7 +302,7 @@ let rec extract_type env db j c args = if Projection.unfolded p then Tunknown else extract_type env db j (mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | _ -> assert false + | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f708307c38..28abb7f575 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -58,7 +58,6 @@ let preamble mod_name comment used_modules usf = else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ str "import qualified GHC.Base" ++ fnl () ++ - str "import qualified GHC.Prim" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "import qualified IOExts" ++ fnl () ++ @@ -78,7 +77,7 @@ let preamble mod_name comment used_modules usf = (if not usf.tunknown then mt () else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ - str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "type Any = GHC.Base.Any" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "type Any = ()" ++ fnl () ++ diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 995d5fd19d..5903733a66 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -486,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str "Please load library " ++ pr_dirpath dp ++ str " first.") + err (str "Please load library " ++ DirPath.print dp ++ str " first.") | _ -> () end | _ -> () diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 1e7da3250b..938bec25b9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -65,11 +65,14 @@ let default_intuition_tac = let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" -VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ - set_default_solver - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> let open Vernacinterp in + set_default_solver + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + ] END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index f660ba7343..d462013353 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -11,7 +11,7 @@ open Formula open Sequent open Rules open Instances -open Term +open Constr open Tacmach.New open Tacticals.New diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index d6309b057f..1a6eba8c62 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -235,8 +235,8 @@ let constant str = Universes.constr_of_global @@ Coqlib.coq_reference "User" ["Init";"Logic"] str let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))] + [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bd5fb1d923..62ca706264 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,7 +1,7 @@ open Printer open CErrors open Util -open Term +open Constr open EConstr open Vars open Namegen @@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) +let pr_leconstr_fp = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let debug_queue = Stack.create () let rec print_debug_queue e = @@ -172,7 +176,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -220,7 +224,8 @@ let find_rectype env sigma c = let isAppConstruct ?(env=Global.env ()) sigma t = try let t',l = find_rectype env sigma t in - observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l))); + observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++ + Printer.pr_leconstr_env env sigma (applist (t',l))); true with Not_found -> false @@ -233,7 +238,8 @@ exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); + observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++ + match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t ); raise NoChange; end in @@ -841,7 +847,7 @@ let build_proof | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam princ_params ); observe (str "fbody_with_full_params := " ++ - pr_leconstr fbody_with_full_params + pr_leconstr_env (Global.env ()) !evd fbody_with_full_params ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 722dbc16b5..7a9bbd92cf 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,8 @@ open Printer open CErrors -open Util open Term +open Sorts +open Util open Constr open Vars open Namegen @@ -115,7 +116,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in - observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); + observe (str "replacing " ++ + pr_lconstr_env env Evd.empty c ++ str " by " ++ + pr_lconstr_env env Evd.empty res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = @@ -345,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in + let univs = + let poly = Flags.is_universe_polymorphism () in + Evd.const_univ_entry ~poly evd' + in + let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant name @@ -565,7 +571,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; - observe (Printer.pr_lconstr scheme_type); + observe (Printer.pr_lconstr_env env sigma scheme_type); let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in @@ -577,8 +583,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let g = fst (decompose_app applied_g) in if Constr.equal f g then raise (Found_type j); - observe (Printer.pr_lconstr f ++ str " <> " ++ - Printer.pr_lconstr g) + observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ + Printer.pr_lconstr_env env sigma g) ) ta; diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 829556a71e..87609296bc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8ab6dbcdf3..fa43536304 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1,7 +1,6 @@ open Printer open Pp open Names -open Term open Constr open Vars open Glob_term @@ -379,29 +378,30 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let open Context.Rel.Declaration in - match decl with + let open Context.Rel.Declaration in + let sigma, _ = Pfedit.get_current_context () in + match decl with | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false | LocalAssum (Name id, t) -> - let new_t = substl ctxt t in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> - let new_t = substl ctxt t in - let new_v = substl ctxt v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ - str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) - ) + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++ + str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + ) (Environ.rel_context new_env) ~init:(env,[]) ) @@ -479,7 +479,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); + observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> @@ -652,8 +652,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); @@ -684,8 +684,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); @@ -897,24 +897,24 @@ let same_raw_term rt1 rt2 = | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = - let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); - let (rhd,lrhs) = glob_decompose_app rhs in - let (lhd,llhs) = glob_decompose_app lhs in - observe (str "lhd := " ++ pr_glob_constr lhd); - observe (str "rhd := " ++ pr_glob_constr rhd); + let _, env = Pfedit.get_current_context () in + let rec decompose_raw_eq lhs rhs acc = + observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr_env env lhd); + observe (str "rhd := " ++ pr_glob_constr_env env rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); - let sllhs = List.length llhs in - let slrhs = List.length lrhs in - if same_raw_term lhd rhd && Int.equal sllhs slrhs + let sllhs = List.length llhs in + let slrhs = List.length lrhs in + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc else (lhs,rhs)::acc in decompose_raw_eq lhs rhs [] - exception Continue (* @@ -923,7 +923,7 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); + observe (str "rebuilding : " ++ pr_glob_constr_env env rt); let open Context.Rel.Declaration in let open CAst in match DAst.get rt with @@ -967,7 +967,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when CErrors.noncritical e -> raise Continue @@ -1012,7 +1012,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let eq' = DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = @@ -1099,7 +1099,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1115,7 +1115,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1134,7 +1134,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index dab094f913..9e22ad3063 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,7 +1,8 @@ open CErrors +open Sorts open Util open Names -open Term +open Constr open EConstr open Pp open Indfun_common @@ -46,7 +47,7 @@ let functional_induction with_clean c princl pat = try find_Function_infos c' with Not_found -> user_err (str "Cannot find induction information on "++ - Printer.pr_leconstr (mkConst c') ) + Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma @@ -74,7 +75,7 @@ let functional_induction with_clean c princl pat = (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) user_err (str "Cannot find induction principle for " - ++Printer.pr_leconstr (mkConst c') ) + ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in let princ = EConstr.of_constr princ in (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') @@ -841,12 +842,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list * let make_graph (f_ref:global_reference) = let c,c_body = match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> - raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) ) - end - | _ -> raise (UserError (None, str "Not a function reference") ) + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + let sigma, env = Pfedit.get_current_context () in + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) + end + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e9102e9c82..8bf6e48fdb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -333,15 +333,17 @@ let discharge_Function (_,finfos) = } let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) + Printer.pr_lconstr_env env sigma + (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -349,7 +351,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in @@ -550,11 +552,11 @@ type tcc_lemma_value = | Value of constr | Not_needed -(* We only "purify" on exceptions *) +(* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try f x with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 692a874d36..694c800514 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -851,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) funs_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b372241d20..9e2774ff32 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -90,20 +90,28 @@ let next_ident_fresh (id:Id.t) = (* comment this line to see debug msgs *) let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c) -let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prconstr c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c) + +let prconstrnl c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") + let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) let prNamedConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); msg(str ""); end let prNamedRConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2fdc3bc37e..b0a76137b7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -9,7 +9,6 @@ module CVars = Vars -open Term open Constr open EConstr open Vars @@ -54,6 +53,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] +let pr_leconstr_rd = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let coq_init_constant s = EConstr.of_constr ( Universes.constr_of_global @@ @@ -63,8 +66,8 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = - let ce = definition_entry ~univs:ctx value (*FIXME *) in +let declare_fun f_id kind ?univs value = + let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) @@ -337,7 +340,8 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p) + let _, env = Pfedit.get_current_context () in + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -455,7 +459,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin @@ -463,7 +467,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -491,8 +495,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> @@ -515,7 +519,7 @@ and travel_args jinfo is_final continuation_tac infos = {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac - (str jinfo.message ++ Printer.pr_leconstr expr_info.info) + (str jinfo.message ++ pr_leconstr_rd expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -731,7 +735,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') + observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac @@ -740,7 +744,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g @@ -991,11 +995,11 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info) + observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos) + (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch @@ -1225,8 +1229,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let p = Proof_global.give_me_the_proof () in - let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in - sigma, List.map (Goal.V82.abstract_type sigma) sgs + let sgs,_,_,_,sigma = Proof.proof p in + sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals let build_and_l sigma l = @@ -1419,7 +1423,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1471,7 +1475,7 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in @@ -1552,8 +1556,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 89feea8dcf..bb01aca558 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c -let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 4b1555e551..982fc7cc3c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -313,30 +313,51 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.universe_context_set sigma in + let poly = Flags.use_polymorphic_flag () in + let ctx = Evd.const_univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) -let add_hints_iff l2r lc n bl = - let l = Locality.LocalityFixme.consume () in - Hints.add_hints (Locality.make_module_locality l) bl +let add_hints_iff ?locality l2r lc n bl = + Hints.add_hints (Locality.make_module_locality locality) bl (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff true lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n bl; + st + end + ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff true lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n ["core"]; + st + end + ] END -VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF + +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff false lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n bl; + st + end + ] | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff false lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n ["core"]; + st + end + ] END (**********************************************************************) @@ -852,34 +873,12 @@ TACTIC EXTEND is_evar ] END -let has_evar sigma c = -let rec has_evar x = - match EConstr.kind sigma x with - | Evar _ -> true - | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ -> - false - | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) -> - has_evar t1 || has_evar t2 - | LetIn (_, t1, t2, t3) -> - has_evar t1 || has_evar t2 || has_evar t3 - | App (t1, ts) -> - has_evar t1 || has_evar_array ts - | Case (_, t1, t2, ts) -> - has_evar t1 || has_evar t2 || has_evar_array ts - | Fix ((_, tr)) | CoFix ((_, tr)) -> - has_evar_prec tr - | Proj (p, c) -> has_evar c -and has_evar_array x = - Array.exists has_evar x -and has_evar_prec (_, ts1, ts2) = - Array.exists has_evar ts1 || Array.exists has_evar ts2 -in -has_evar c - TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") + if Evarutil.has_undefined_evars sigma x + then Proofview.tclUNIT () + else Tacticals.New.tclFAIL 0 (str "No evars") ] END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 5baa0d5c1d..90a44708fc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -51,8 +51,12 @@ let eval_uconstrs ist cs = List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) ARGUMENT EXTEND auto_using TYPED AS uconstr_list @@ -186,7 +190,7 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c let glob_hints_path ist = Hints.glob_hints_path - + ARGUMENT EXTEND hints_path PRINTED BY pr_hints_path @@ -210,10 +214,15 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (match dbnames with None -> ["core"] | Some l -> l) entry ] + fun ~atts ~st -> begin + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints (Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + st + end + ] END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 1161525689..34fea6175b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -469,13 +469,13 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] END -VERNAC COMMAND EXTEND VernacTacticNotation +VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => [ VtUnknown, VtNow ] -> - [ - let l = Locality.LocalityFixme.consume () in - let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e + [ fun ~atts ~st -> let open Vernacinterp in + let n = Option.default 0 n in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + st ] END @@ -512,15 +512,15 @@ PRINTED BY pr_tacdef_body | [ tacdef_body(t) ] -> [ t ] END -VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ((_,r),_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater - ] -> [ - let lc = Locality.LocalityFixme.consume () in - Tacentries.register_ltac (Locality.make_module_locality lc) l + ] -> [ fun ~atts ~st -> let open Vernacinterp in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + st ] END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index fea9e837b1..f6cc3833a7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -123,11 +123,15 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF | [ "Admit" "Obligations" ] -> [ admit_obligations None ] END -VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> begin + let open Vernacinterp in + set_default_tactic + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + end] END open Pp diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b148d962ed..ea1808a255 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings -let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge))) -let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge)) +let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst (snd ge))) +let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst ge)) let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l @@ -239,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END -VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + st + ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + st + ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + st + ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + st + ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + st + ] END TACTIC EXTEND setoid_symmetry @@ -272,5 +291,7 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> + [ let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 38460c669f..d707512457 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,14 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (na,(bl,t)) = + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) + str " :=" ++ brk (1,1) ++ pr t) - let pr_let_clauses recflag pr = function + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -1003,7 +1020,7 @@ let pr_goal_selector ~toplevel s = | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> @@ -1226,6 +1243,15 @@ let make_constr_printer f c = let lift f a = Genprint.PrinterBasic (fun () -> f a) + +let pr_glob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_glob_constr_env env c + +let pr_lglob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_lglob_constr_env env c + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1240,7 +1266,7 @@ let () = Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) + (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl @@ -1251,45 +1277,45 @@ let () = Genprint.register_print0 wit_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr - (fun (c,_) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) pr_red_expr_env ; Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_bindings_env ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 wit_open_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_destruction_arg_env ; Genprint.register_print0 Stdarg.wit_int int int (lift int); diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 705a51edd3..c0060c5a7c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pp open CErrors open Util +open Names open Nameops open Namegen open Constr @@ -1143,7 +1143,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in @@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma = in anew_instance global binders instance [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] -let declare_relation ?(binders=[]) a aeq n refl symm trans = +let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in + let global = not (Locality.make_section_locality locality) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in ignore(anew_instance global binders instance []); match (refl,symm,trans) with @@ -1884,11 +1884,11 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.const_univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:ctx term + Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1972,9 +1972,10 @@ let add_morphism_infer glob m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then + let uctx = UState.const_univ_entry ~poly uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,UState.context uctx),None), + (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1306c590ba..17e7244b39 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -75,7 +75,7 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : +val declare_relation : ?locality:bool -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 180fb2db40..918d1faebe 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -91,9 +91,10 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (is_global ref' t') then - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ - pr_global ref') ; + (let sigma, env = Pfedit.get_current_context () in + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ + pr_global ref')); ref' in subst_or_var (subst_located subst_global) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index a669692fc9..2dd7c9a747 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> Printer.pr_constr_pattern p) rl + (fun (_,p) -> + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + let sigma, env = Pfedit.get_current_context () in + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 218342efe4..cb54cac3f1 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -984,7 +984,9 @@ struct let parse_expr sigma parse_constant parse_exp ops_spec env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term); + then ( + let _, env = Pfedit.get_current_context () in + Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); (* let constant_or_variable env term = @@ -1103,9 +1105,10 @@ struct | _ -> raise ParseError - let rconstant sigma term = + let rconstant sigma term = + let _, env = Pfedit.get_current_context () in if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1145,9 +1148,9 @@ struct let parse_arith parse_op parse_expr env cstr gl = let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); - match EConstr.kind sigma cstr with + if debug + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); + match EConstr.kind sigma cstr with | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in @@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr ff); + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; @@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' + (dump_cstr spec.typ spec.dump_coeff) ff' in + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; (* Even if it does not work, this does not mean it is not provable diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 7da4a3b829..52c6ef983d 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' = (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) -let and_cnf f1 f2 = - app f1 f2 +let and_cnf = + app (** val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 @@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb +let norm = + norm_aux (** val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb = - psub cO cplus cminus copp ceqb +let psub0 = + psub (** val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let padd0 cO cplus ceqb = - padd cO cplus ceqb +let padd0 = + padd (** val xnormalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ff69ddefb8..8692842468 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -466,12 +466,14 @@ let destructurate_prop sigma t = | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo -let destructurate_type sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let c, args = decompose_app sigma t in +let nf = Tacred.simpl + +let destructurate_type env sigma t = + let is_conv = Reductionops.is_conv env sigma in + let c, args = decompose_app sigma (nf env sigma t) in match EConstr.kind sigma c, args with - | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args) - | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args) + | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args) + | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args) | _ -> Kufo let destructurate_term sigma t = @@ -1459,17 +1461,13 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = else (tactic,defs) -let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c - -let destructure_omega gl tac_def (id,c) = - let open Tacmach.New in - let sigma = project gl in +let destructure_omega env sigma tac_def (id,c) = if String.equal (atompart_of_id id) "State" then tac_def else try match destructurate_prop sigma c with | Kapp(Eq,[typ;t1;t2]) - when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end -> + when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end -> let t = mk_plus t1 (mk_inv t2) in normalize_equation sigma id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def @@ -1507,7 +1505,7 @@ let coq_omega = Proofview.Goal.enter begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in - let destructure_omega = destructure_omega gl in + let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in let tactic_normalisation, system = List.fold_left destructure_omega ([],[]) hyps_types in let prelude,sys = @@ -1727,27 +1725,26 @@ let not_binop = function exception Undecidable -let rec decidability gl t = - let open Tacmach.New in - match destructurate_prop (project gl) t with +let rec decidability env sigma t = + match destructurate_prop sigma t with | Kapp(Or,[t1;t2]) -> mkApp (Lazy.force coq_dec_or, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kapp(And,[t1;t2]) -> mkApp (Lazy.force coq_dec_and, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kapp(Iff,[t1;t2]) -> mkApp (Lazy.force coq_dec_iff, [| t1; t2; - decidability gl t1; decidability gl t2 |]) + decidability env sigma t1; decidability env sigma t2 |]) | Kimp(t1,t2) -> (* This is the only situation where it's not obvious that [t] is in Prop. The recursive call on [t2] will ensure that. *) mkApp (Lazy.force coq_dec_imp, - [| t1; t2; decidability gl t1; decidability gl t2 |]) + [| t1; t2; decidability env sigma t1; decidability env sigma t2 |]) | Kapp(Not,[t1]) -> - mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |]) + mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |]) | Kapp(Eq,[typ;t1;t2]) -> - begin match destructurate_type (project gl) (pf_nf gl typ) with + begin match destructurate_type env sigma typ with | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) | _ -> raise Undecidable @@ -1784,15 +1781,16 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - let decidability = decidability gl in - let pf_nf = pf_nf gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in let rec loop = function | [] -> (tclTHEN nat_inject coq_omega) | LocalDef (i,body,typ) :: lit when !letin_flag -> Proofview.tclEVARMAP >>= fun sigma -> begin try - match destructurate_type sigma (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) | Kapp(Z,_) -> let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in let hty = mk_gen_eq typ (mkVar i) body in @@ -1895,7 +1893,7 @@ let destructure_hyps = with Not_found -> loop lit) | Kapp(Eq,[typ;t1;t2]) -> if !old_style_flag then begin - match destructurate_type sigma (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) -> tclTHENLIST [ (simplest_elim @@ -1912,7 +1910,7 @@ let destructure_hyps = ] | _ -> loop lit end else begin - match destructurate_type sigma (pf_nf typ) with + match destructurate_type env sigma typ with | Kapp(Nat,_) -> (tclTHEN (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) @@ -1940,7 +1938,9 @@ let destructure_hyps = let destructure_goal = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let decidability = decidability gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let decidability = decidability env sigma in let rec loop t = Proofview.tclEVARMAP >>= fun sigma -> let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 96bf31b11a..0ea8904f2c 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -104,7 +104,7 @@ open CErrors open Util open Names -open Term +open Constr open EConstr open Pattern open Patternops diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5397b00656..337510ef1f 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,7 +7,6 @@ *************************************************************************) open Names -open Term open Constr let module_refl_name = "ReflOmegaCore" @@ -198,6 +197,7 @@ let parse_logic_rel c = match destructurate c with (* Binary numbers *) +let coq_Z = lazy (bin_constant "Z") let coq_xH = lazy (bin_constant "xH") let coq_xO = lazy (bin_constant "xO") let coq_xI = lazy (bin_constant "xI") @@ -238,7 +238,7 @@ end module Z : Int = struct -let typ = lazy (bin_constant "Z") +let typ = coq_Z let plus = lazy (z_constant "Z.add") let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") @@ -286,14 +286,9 @@ let parse_term t = (match recognize_Z t with Some t -> Tnum t | None -> Tother) | _ -> Tother -let pf_nf gl c = - EConstr.Unsafe.to_constr - (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c)) - let is_int_typ gl t = - match destructurate (pf_nf gl t) with - | Kapp("Z",[]) -> true - | _ -> false + Tacmach.New.pf_apply Reductionops.is_conv gl + (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) let parse_rel gl t = match destructurate t with diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 430b608f4c..54ff44fbd3 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -183,8 +183,9 @@ let print_env_reification env = let rec loop c i = function [] -> str " ===============================\n\n" | t :: l -> + let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 447acb9057..8e4d8b0d34 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -41,9 +41,12 @@ Ltac Ss_to_add f acc := | _ => constr:((acc + f)%nat) end. +(* For internal use only *) +Local Definition protected_to_nat := N.to_nat. + Ltac natprering := match goal with - |- context C [S ?p] => + |- context C [S ?p] => match p with O => fail 1 (* avoid replacing 1 with 1+0 ! *) | p => match isnatcst p with @@ -52,9 +55,19 @@ Ltac natprering := fold v; natprering end end - | _ => idtac + | _ => change N.to_nat with protected_to_nat + end. + +Ltac natpostring := + match goal with + | |- context [N.to_nat ?x] => + let v := eval cbv in (N.to_nat x) in + change (N.to_nat x) with v; + natpostring + | _ => change protected_to_nat with N.to_nat end. Add Ring natr : natSRth - (morphism nat_morph_N, constants [natcst], preprocess [natprering]). + (morphism nat_morph_N, constants [natcst], + preprocess [natprering], postprocess [natpostring]). diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 05ab8ab326..a7d6d5bb20 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) ) !from_name ] END @@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) ) !field_from_name ] END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9e4b896f8e..f22f00839a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -150,13 +150,13 @@ let ic_unsafe c = (*FIXME remove *) let sigma = Evd.from_env env in EConstr.of_constr (fst (Constrintern.interp_constr env sigma c)) -let decl_constant na ctx c = +let decl_constant na univs c = let open Constr in let vars = Univops.universes_of_constr c in - let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + let univs = Univops.restrict_universe_context univs vars in + let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true - ~univs:(Univ.ContextSet.to_context ctx) c), + (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) (* Calling a global tactic *) @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) + Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -344,8 +344,6 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -let pr_constr c = pr_econstr c - module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -368,7 +366,7 @@ let find_ring_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) | [] -> assert false let add_entry (sp,_kn) e = @@ -529,19 +527,19 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\","++spc()++ str"\""++pr_constr mul_m_lem++ - str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ + str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ str"\""++spc()++str"and \""++ - pr_constr mul_m_lem++str"\""); + pr_econstr_env env !evd mul_m_lem++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) @@ -861,7 +859,7 @@ let find_field_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) | [] -> assert false let add_field_entry (sp,_kn) e = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index c1d7e62785..047ca509be 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -240,7 +240,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c)); + ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); (sigma, (sigma, c)) @@ -539,7 +539,7 @@ module Intset = Evar.Set let pf_abs_evars_pirrel gl (sigma, c0) = pp(lazy(str"==PF_ABS_EVARS_PIRREL==")); - pp(lazy(str"c0= " ++ Printer.pr_constr c0)); + pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0)); let sigma0 = project gl in let c0 = nf_evar sigma0 (nf_evar sigma c0) in let nenv = env_size (pf_env gl) in @@ -563,9 +563,9 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") - (fun (k,_) -> str(Evd.string_of_existential k)) evlist)); + (fun (k,_) -> Evar.print k) evlist)); let evplist = let depev = List.fold_left (fun evs (_,(_,t,_)) -> let t = EConstr.of_constr t in @@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in - pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t)); + pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Tacmach.refine_no_check t gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = @@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = compose_lam (let xs,y = List.chop (n-1) l in y @ xs) (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) in - pp(lazy(str"after: " ++ Printer.pr_constr oc)); + pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc)); try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error @@ -1202,7 +1202,7 @@ let genclrtac cl cs clr = let gentac ist gen gl = (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr c)); + ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 26b5c57675..4e0b44a44d 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma = if not (EConstr.eq_constr sigma t t') then loop ctx t' else errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++ str"A (applied) bound variable was expected as the conclusion of "++ - str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in + str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in let n_elim_args = Context.Rel.nhyps ctx in let is_rec_elim = @@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr c)); + ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr | Some (c, _, _,gl) -> true, gl | None -> errorstrm Pp.(str"Unable to apply the eliminator to the term"++ - spc()++pr_econstr c++spc()++str"or to unify it's type with"++ - pr_econstr inf_arg_ty) in + spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++ + pr_econstr_env env (project gl) inf_arg_ty) in ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index e82f222b9c..bd9633afbd 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -77,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt)); + ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -86,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term ist gl t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -109,7 +109,7 @@ let congrtac ((n, t), ty) ist gl = let newssrcongrtac arg ist gl = ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -247,7 +247,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr c)), + ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -267,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl = | Proj _ when same_proj sigma0 c t -> body env t c | Const f -> aux (body env c c) | App (f, a) -> aux (EConstr.mkApp (body env f f, a)) - | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++ - str" contains no " ++ pr_econstr t ++ str" even after unfolding") + | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++ + str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding") in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c) else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in @@ -342,7 +342,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) - let elim, _ = Term.destConst elim in + let elim, _ = destConst elim in let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in @@ -352,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* We check the proof is well typed *) let sigma, proof_ty = try Typing.type_of env sigma proof with _ -> raise PRtype_error in - ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty)); + ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl with _ -> @@ -374,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) | _ -> anomaly "rewrite rule not an application" in - errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++ - (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty)) + errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++ + (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; let is_construct_ref sigma c r = @@ -391,12 +391,12 @@ let rwcltac cl rdx dir sr gl = let gl = pf_unsafe_merge_uc ucst gl in let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr))); + ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = if EConstr.Vars.closed0 (project gl) r' then let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty)); + ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in @@ -411,7 +411,7 @@ let rwcltac cl rdx dir sr gl = let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr)) - ++ str " to " ++ pr_econstr r2) in + ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in @@ -605,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in - let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in Feedback.msg_info Pp.(str"BEGIN INSTANCES"); try while true do diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 29e96ec59f..5c1b399a80 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,11 +8,12 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Pp open Names +open Constr open Tacmach open Ssrmatching_plugin.Ssrmatching - open Ssrprinters open Ssrcommon open Ssrtacticals @@ -30,10 +31,6 @@ let ssrposetac ist (id, (_, t)) gl = let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) -open Pp -open Term -open Constr - let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl = let pat = interp_cpattern ist gl pat (Option.map snd pty) in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in @@ -72,13 +69,14 @@ let examine_abstract id gl = let gl, tid = pfe_type_of gl id in let abstract, gl = pf_mkSsrConst "abstract" gl in let sigma = project gl in + let env = pf_env gl in if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then - errorstrm(strbrk"not an abstract constant: "++pr_econstr id); + errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id); let _, args_id = EConstr.destApp sigma tid in if Array.length args_id <> 3 then - errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id); + errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id); if not (is_Evar_or_CastedMeta sigma args_id.(2)) then - errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used"); + errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used"); tid, args_id let pf_find_abstract_proof check_lock gl abstract_n = @@ -94,7 +92,7 @@ let pf_find_abstract_proof check_lock gl abstract_n = | _ -> l) (project gl) [] in match l with | [e] -> e - | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++ strbrk" not found in the evar map exactly once. "++ strbrk"Did you tamper with it?") @@ -205,7 +203,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function @@ -271,7 +269,7 @@ let ssrabstract ist gens (*last*) gl = let gl, proof = let pf_unify_HO gl a b = try pf_unify_HO gl a b - with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++ + with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++ strbrk" cannot abstract this goal. Did you generalize it?") in let find_hole p t = match EConstr.kind (project gl) t with @@ -290,7 +288,7 @@ let ssrabstract ist gens (*last*) gl = | App(hd, [|left; right|]) when Term.Constr.equal hd prod -> find_hole (mkApp (proj1,[|left;right;p|])) left *) - | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++ strbrk" has an unexpected shape. Did you tamper with it?") in find_hole @@ -361,14 +359,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Sort _, [] -> EConstr.Vars.subst_vars s ct | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) - | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in let c = var2rel c gens [] in let rec pired c = function | [] -> c | t::ts as args -> match EConstr.kind sigma c with | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args) - | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in c, args, pired c args, pf_merge_uc uc gl in let tacipat pats = introstac ~ist pats in let tacigens = @@ -396,8 +394,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Some id -> if pats = [] then Tacticals.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++pr_econstr ct)); + ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); + ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); Tacticals.tclTHENS (basecuttac "ssr_have" ct) [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in "ssr_have", diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 023778fdbf..6c325cce43 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl = (* Utils of local interest only *) let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in - ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in + ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in let protectC, gl = pf_mkSsrConst "protect_term" gl in let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in let eq = EConstr.of_constr eq in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7b591feada..46403aef3c 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function | (fk, h), (_, (_, Some c)) -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | (fk, h), (_, (c, None)) -> - pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) + pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c) let pr_unguarded prc prlc = prlc diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e865ef706d..4b2fab6d19 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs -> hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs let pp_term gl t = - let t = Reductionops.nf_evar (project gl) t in pr_econstr t + let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t (* FIXME *) (* terms are pre constr, the kind is parsing/printing flag to distinguish diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 36dce37aea..3efb7b9147 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -158,11 +158,14 @@ let declare_one_prenex_implicit locality f = | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] -VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF | [ "Prenex" "Implicits" ne_global_list(fl) ] - -> [ let locality = - Locality.make_section_locality (Locality.LocalityFixme.consume ()) in - List.iter (declare_one_prenex_implicit locality) fl ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + let locality = Locality.make_section_locality atts.locality in + List.iter (declare_one_prenex_implicit locality) fl; + st + ] END (* Vernac grammar visibility patch *) @@ -343,7 +346,7 @@ let coerce_search_pattern_to_sort hpat = let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ - pr_constr_pattern hpat') in + pr_constr_pattern_env env sigma hpat') in if EConstr.isSort sigma ht then begin warn (); true, hpat' end else let filter_head, coe_path = try @@ -359,7 +362,7 @@ let coerce_search_pattern_to_sort hpat = let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc () + errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path @@ -468,10 +471,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref c = match DAst.get c with +let pr_rawhintref c = + let _, env = Pfedit.get_current_context () in + match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr c + pr_glob_constr_env env f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c @@ -546,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d )) + Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), + ((Loc.tag s),None),(d ))) ]]; END diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d5c9e4988e..e63a05b781 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -100,7 +100,6 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let pr_constr = pr_constr let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr @@ -397,7 +396,7 @@ let inv_dir = function L2R -> R2L | R2L -> L2R type pattern_class = | KpatFixed | KpatConst - | KpatEvar of existential_key + | KpatEvar of Evar.t | KpatLet | KpatLam | KpatRigid @@ -427,7 +426,8 @@ let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = if isEvar c then hole_var else map wipe_evar c in - pr_constr (wipe_evar c0) + let sigma, env = Pfedit.get_current_context () in + pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = @@ -1215,7 +1215,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in let e_body = match e_body with Evar_defined c -> c - | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++ + | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++ str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ str "in the pattern?") in @@ -1417,7 +1417,8 @@ let ssrinstancesof ist arg gl = let find, conclude = mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma None (etpat,[tpat]) in - let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in ppnl (str"BEGIN INSTANCES"); try while true do |