diff options
84 files changed, 768 insertions, 405 deletions
@@ -5,6 +5,39 @@ Vernacular commands - New command "Redirect" to redirect the output of a command to a file. +Tactics + +- New flag "Regular Subst Tactic" which fixes "subst" in situations where + it failed to substitute all substitutable equations or failed to simplify + cycles, or accidentally unfolded local definitions (flag is off by default). +- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a + special way. It accepts three distinct flags: + * "Lax", which is the default one, sets the old behavior, i.e. a non-imported + hint behaves the same as an imported one. + * "Warn" outputs a warning when a non-imported hint is used. Note that this is + an over-approximation, because a hint may be triggered by an eauto run that + will eventually fail and backtrack. + * "Strict" changes the behavior of an unloaded hint to the one of the fail + tactic, allowing to emulate the hopefully future import-scoped hint mechanism. + +API + +- Some functions from pretyping/typing.ml and their derivatives were potential + source of evarmap leaks, as they dropped their resulting evarmap. The + situation was clarified by renaming them according to a unsafe_* scheme. Their + sound variant is likewise renamed to their old name. The following renamings + were made. + * Typing.type_of -> unsafe_type_of + * Typing.e_type_of -> type_of + * A new e_type_of function that matches the e_ prefix policy + * Tacmach.pf_type_of -> pf_unsafe_type_of + * A new safe pf_type_of function. + All uses of unsafe_* functions should be eventually eliminated. + + +Tools + +- Added an option -w to control the output of coqtop warnings. Changes from V8.5beta1 to V8.5beta2 =================================== @@ -19,7 +52,6 @@ Tactics - A script using the admit tactic can no longer be concluded by either Qed or Defined. In the first case, Admitted can be used instead. In the second case, a subproof should be used. - - The easy tactic and the now tactical now have a more predictable behavior, but they might now discharge some previously unsolved goals. @@ -27,25 +59,21 @@ Extraction - Definitions extracted to Haskell GHC should no longer randomly segfault when some Coq types cannot be represented by Haskell types. - - Definitions can now be extracted to Json for post-processing. Tools - Option -I -as has been removed, and option -R -as has been deprecated. In both cases, option -R can be used instead. - - coq_makefile now generates double-colon rules for rules such as clean. API - The interface of [change] has changed to take a [change_arg], which can be built from a [constr] using [make_change_arg]. - - [pattern_of_constr] now returns a triplet including the cleaned-up [evar_map], removing the evars that were turned into metas. - Changes from V8.4 to V8.5beta1 ============================== diff --git a/Makefile.build b/Makefile.build index 8f64d1ff2..a790b92b2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -81,7 +81,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) +COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands diff --git a/configure.ml b/configure.ml index 267d556a2..e21088584 100644 --- a/configure.ml +++ b/configure.ml @@ -1199,7 +1199,9 @@ let write_makefile f = pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; pr "# Option to control compilation and installation of the documentation\n"; - pr "WITHDOC=%s\n" (if withdoc then "all" else "no"); + pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); + pr "# Option to produce precompiled files for native_compute\n"; + pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2eebac18e..be82eaa01 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2803,6 +2803,7 @@ This tactic is deprecated. It can be replaced by {\tt enough} \subsection{\tt subst \ident} \tacindex{subst} +\optindex{Regular Subst Tactic} This tactic applies to a goal that has \ident\ in its context and (at least) one hypothesis, say {\tt H}, of type {\tt @@ -2822,6 +2823,26 @@ When several hypotheses have the form {\tt \ident=t} or {\tt Applies {\tt subst} repeatedly to all identifiers from the context for which an equality exists. + +\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set + Regular Subst Tactic}. When this option is activated, {\tt subst} + manages the following corner cases which otherwise it + does not: +\begin{itemize} +\item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$} + and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a + variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$} + or {\tt $u$ = \ident$_2$} +\item A context with cyclic dependencies as with hypotheses {\tt + \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} +\end{itemize} +Additionally, it prevents a local definition such as {\tt \ident := + $t$} to be unfolded which otherwise it would exceptionally unfold in +configurations containing hypotheses of the form {\tt {\ident} = $u$}, +or {\tt $u'$ = \ident} with $u'$ not a variable. + +The option is off by default. + \end{Variants} \subsection{\tt stepl \term} @@ -3853,6 +3874,7 @@ development. \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ \mbox{\dots} \ident$_m$} +\label{RemoveHints} \comindex{Remove Hints} This command removes the hints associated to terms \term$_1$ \mbox{\dots} @@ -3931,8 +3953,9 @@ main subgoal excluded. \end{Variants} -\subsection{Hints and sections -\label{Hint-and-Section}} +\subsection{Hint locality +\label{Hint-Locality}} +\optindex{Loose Hint Behavior} Hints provided by the \texttt{Hint} commands are erased when closing a section. Conversely, all hints of a module \texttt{A} that are not @@ -3940,6 +3963,43 @@ defined inside a section (and not defined with option {\tt Local}) become available when the module {\tt A} is imported (using e.g. \texttt{Require Import A.}). +As of today, hints only have a binary behavior regarding locality, as described +above: either they disappear at the end of a section scope, or they remain +global forever. This causes a scalability issue, because hints coming from an +unrelated part of the code may badly influence another development. It can be +mitigated to some extent thanks to the {\tt Remove Hints} command +(see ~\ref{RemoveHints}), but this is a mere workaround and has some +limitations (for instance, external hints cannot be removed). + +A proper way to fix this issue is to bind the hints to their module scope, as +for most of the other objects Coq uses. Hints should only made available when +the module they are defined in is imported, not just required. It is very +difficult to change the historical behavior, as it would break a lot of scripts. +We propose a smooth transitional path by providing the {\tt Loose Hint Behavior} +option which accepts three flags allowing for a fine-grained handling of +non-imported hints. + +\begin{Variants} + +\item {\tt Set Loose Hint Behavior "Lax"} + + This is the default, and corresponds to the historical behavior, that is, + hints defined outside of a section have a global scope. + +\item {\tt Set Loose Hint Behavior "Warn"} + + When set, it outputs a warning when a non-imported hint is used. Note that + this is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being actually + useful for the proof. + +\item {\tt Set Loose Hint Behavior "Strict"} + + When set, it changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. + +\end{Variants} + \subsection{Setting implicit automation tactics} \subsubsection{\tt Proof with {\tac}} diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 02e43361a..f6fd27dd8 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -163,17 +163,17 @@ let is_constr_gram = function | Aentry ("constr", "constr") -> true | _ -> false -let make_vars len = - (** We choose names unlikely to be written by a human, even though that - does not matter at all. *) - List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i))) +let make_var = function + | GramNonTerminal(loc',_,_,Some p) -> Some p + | GramNonTerminal(loc',_,_,None) -> Some (Id.of_string "_") + | _ -> assert false let declare_tactic loc s c cl = match cl with | [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in - let vars = make_vars (List.length rem) in + let vars = List.map make_var rem in let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b12d29d6c..1f3fa3ed3 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util + class type proof_view = object inherit GObj.widget @@ -162,12 +164,21 @@ let display mode (view : #GText.view_skel) goals hints evars = List.iter iter shelved_goals | _, _, _, _ -> (* No foreground proofs, but still unfocused ones *) - view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; - let iter goal = + let total = List.length bg in + let goal_str index = Printf.sprintf + "______________________________________(%d/%d)\n" index total + in + let vb, pl = if total = 1 then "is", "" else "are", "s" in + let msg = Printf.sprintf "This subproof is complete, but there %s still %d \ + unfocused goal%s:\n\n" vb total pl + in + let () = view#buffer#insert msg in + let iter i goal = + let () = view#buffer#insert (goal_str (succ i)) in let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in view#buffer#insert msg in - List.iter iter bg + List.iteri iter bg end | Some { Interface.fg_goals = fg } -> mode view fg hints diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca814f497..4c1614bac 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -213,8 +213,8 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a let cst = instantiate_inductive_constraints mib u in (ty, cst) -let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = - type_of_inductive_gen env mip args +let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = + type_of_inductive_gen ~polyprop env mip args (* The max of an array of universes *) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 75a3fc458..1f8bfc984 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -121,9 +121,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 let native_conv pb sigma env t1 t2 = - if !Flags.no_native_compiler then begin - let msg = "Native compiler is disabled, "^ - "falling back to VM conversion test." in + if Coq_config.no_native_compiler then begin + let msg = "Native compiler is disabled, falling back to VM conversion test." in Pp.msg_warning (Pp.str msg); vm_conv pb env t1 t2 end diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d762a246e..d6bd75478 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -772,9 +772,9 @@ let export ?except senv dir = } in let ast, values = - if !Flags.no_native_compiler then [], [||] - else + if !Flags.native_compiler then Nativelibrary.dump_library mp dir senv.env str + else [], [||] in let lib = { comp_name = dir; diff --git a/lib/flags.ml b/lib/flags.ml index c8e7f7afe..313da0c5b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -160,7 +160,7 @@ let make_polymorphic_flag b = let program_mode = ref false let is_program_mode () = !program_mode -let warn = ref true +let warn = ref false let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x @@ -206,8 +206,8 @@ let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level -(* Disabling native code compilation for conversion and normalization *) -let no_native_compiler = ref Coq_config.no_native_compiler +(* Native code compilation for conversion and normalization *) +let native_compiler = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 756d3b851..1f68a88f3 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -128,8 +128,8 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(* Disabling native code compilation for conversion and normalization *) -val no_native_compiler : bool ref +(* Native code compilation for conversion and normalization *) +val native_compiler : bool ref (* Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref diff --git a/lib/terminal.ml b/lib/terminal.ml index 0f6b23af3..58851ed27 100644 --- a/lib/terminal.ml +++ b/lib/terminal.ml @@ -117,7 +117,7 @@ let is_extended = function | `INDEX _ | `RGB _ -> true | _ -> false -let eval st = +let repr st = let fg = match st.fg_color with | None -> [] | Some c -> @@ -152,7 +152,10 @@ let eval st = | Some true -> [7] | Some false -> [27] in - let tags = fg @ bg @ bold @ italic @ underline @ negative in + fg @ bg @ bold @ italic @ underline @ negative + +let eval st = + let tags = repr st in let tags = List.map string_of_int tags in Printf.sprintf "\027[%sm" (String.concat ";" tags) diff --git a/lib/terminal.mli b/lib/terminal.mli index f308ede32..49172e3ce 100644 --- a/lib/terminal.mli +++ b/lib/terminal.mli @@ -46,6 +46,9 @@ val make : ?fg_color:color -> ?bg_color:color -> val merge : style -> style -> style (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *) +val repr : style -> int list +(** Generate the ANSI code representing the given style. *) + val eval : style -> string (** Generate an escape sequence from a style. *) diff --git a/library/library.ml b/library/library.ml index 1ffa1a305..0296d7b90 100644 --- a/library/library.ml +++ b/library/library.ml @@ -166,7 +166,7 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if not !Flags.no_native_compiler then + if !Flags.native_compiler then Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function @@ -788,10 +788,10 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if not !Flags.no_native_compiler then + if !Flags.native_compiler then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then - msg_error (str"Could not compile the library to native code. Skipping.") + error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in let () = msg_warning (str "Removed file " ++ str f') in diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 29bca8622..d5d6bdf74 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -513,7 +513,7 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_type_of state.gls trm in + let typ = pf_unsafe_type_of state.gls trm in let typ = canonize_name typ in let new_node= match t with @@ -836,7 +836,7 @@ let complete_one_class state i= let _,etyp,rest= destProd typ in let id = new_state_var etyp state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_type_of state.gls + let _c = pf_unsafe_type_of state.gls (constr_of_term (term state.uf pac.cnode)) in let _args = List.map (fun i -> constr_of_term (term state.uf i)) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 05f4c4903..9c3a0f729 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -253,9 +253,15 @@ let new_app_global f args k = let new_refine c = Proofview.V82.tactic (refine c) +let assert_before n c = + Proofview.Goal.enter begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) + end + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of t = Tacmach.New.pf_type_of gl t in + let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check c @@ -325,7 +331,7 @@ let refute_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl in let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in @@ -335,14 +341,14 @@ let refute_tac c t1 t2 p = end let refine_exact_check c gl = - let evm, _ = pf_apply e_type_of gl c in + let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl in let neweq= new_app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in @@ -367,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.nf_enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl in let concl = Proofview.Goal.concl gl in (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) @@ -376,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p = (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_type_of gls identity in *) + (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in let outtype = mkSort outtype in @@ -480,7 +486,7 @@ let congruence_tac depth l = let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) let ty = (* Termops.refresh_universes *) (type_of c1) in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 36273faae..714cd8634 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -773,7 +773,7 @@ let rec take_tac wits gls = match wits with [] -> tclIDTAC gls | wit::rest -> - let typ = pf_type_of gls wit in + let typ = pf_unsafe_type_of gls wit in tclTHEN (thus_tac wit typ []) (take_tac rest) gls @@ -854,7 +854,7 @@ let start_tree env ind rp = let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in let (ind,u) = @@ -869,7 +869,7 @@ let build_per_info etype casee gls = | _ -> mind.mind_nparams,None in let params,real_args = List.chop nparams args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let pred= List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in @@ -1228,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let nparams = mind.mind_nparams in let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in let ind', u = destInd hd in let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5912f0a0c..c80a8081a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -105,7 +105,7 @@ let mk_open_instance id idc gl m t= let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_type_of gl idc in + let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in @@ -154,7 +154,7 @@ let left_instance_tac (inst,id) continue seq= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in let evmap, _ = - try Typing.e_type_of (pf_env gl) evmap gt + try Typing.type_of (pf_env gl) evmap gt with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7d034db55..96c4eb01e 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl = let l = expand_constructor_hints l in let f gr (seq,gl) = let gl, c = pf_eapply Evd.fresh_global gl gr in - let typ=(pf_type_of gl c) in + let typ=(pf_unsafe_type_of gl c) in (add_formula Hyp gr typ seq gl,gl) in List.fold_right f l (seq,gl) @@ -209,12 +209,12 @@ open Hints let extend_with_auto_hints l seq gl= let seqref=ref seq in let f p_a_t = - match repr_auto_tactic p_a_t.code with + match repr_hint p_a_t.code with Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> (try let gr = global_of_constr c in - let typ=(pf_type_of gl c) in + let typ=(pf_unsafe_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4a832435f..169a70600 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -328,7 +328,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let all_ids = pf_ids_of_hyps g in let new_ids,_ = list_chop ctxt_size all_ids in let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.e_type_of g to_refine in + let evm, _ = pf_apply Typing.type_of g to_refine in tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g ) in @@ -543,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -593,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) - let new_term_value_eq = pf_type_of g' (mkVar heq_id) in + let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in (* compute the new value of the body *) let new_term_value = match kind_of_term new_term_value_eq with @@ -606,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = in let fun_body = mkLambda(Anonymous, - pf_type_of g' term, + pf_unsafe_type_of g' term, Termops.replace_term term (mkRel 1) dyn_infos.info ) in @@ -638,7 +638,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in - let evm, _ = pf_apply Typing.e_type_of g c in + let evm, _ = pf_apply Typing.type_of g c in tclTHENLIST[ Refiner.tclEVARS evm; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); @@ -699,7 +699,7 @@ let build_proof let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in + let type_of_term = pf_unsafe_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -919,7 +919,7 @@ let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_type_of g (mkVar hyp) in + let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if Id.List.mem hyp hyps @@ -964,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = - let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f + let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f in decompose_prod_n_assum (nb_params + nb_args) t,evd @@ -1034,8 +1034,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in - let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in - evd:=evd'; + evd:=evd'; + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in let nb_intro_to_do = nb_prod (pf_concl g) in @@ -1414,7 +1414,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in + let _,hrec_concl = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in let f_app = Array.last (snd (destApp hrec_concl)) in let f = (fst (destApp f_app)) in let rec backtrack : tactic = @@ -1641,7 +1641,7 @@ let prove_principle_for_gen (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1)); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *) +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a2bbf97ae..3edc590cc 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -274,7 +274,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") [] in - let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -327,7 +327,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let s = Universes.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in - let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in + let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in ignore( @@ -478,7 +478,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr in let _ = evd := sigma in let l_schemes = - List.map (Typing.type_of env sigma) schemes + List.map (Typing.unsafe_type_of env sigma) schemes in let i = ref (-1) in let sorts = @@ -608,8 +608,8 @@ let build_scheme fas = (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in - let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in - let _ = evd := evd' in + let _ = evd := evd' in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in (destConst f,sort) ) fas @@ -659,7 +659,7 @@ let build_case_scheme fa = in let sigma, scheme = (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in - let scheme_type = (Typing.type_of env sigma ) scheme in + let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 043d4328c..61f03d6f2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -321,7 +321,7 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = - let typ = Tacmach.pf_type_of gl cstr in + let typ = Tacmach.pf_unsafe_type_of gl cstr in tclTHEN (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)) (tclTHENFIRST @@ -349,7 +349,7 @@ let rec poseq_list_ids_rec lcstr gl = let _ = prstr "c = " in let _ = prconstr c in let _ = prstr "\n" in - let typ = Tacmach.pf_type_of gl c in + let typ = Tacmach.pf_unsafe_type_of gl c in let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in let x = Tactics.fresh_id [] cname gl in let _ = list_constr_largs:=mkVar x :: !list_constr_largs in @@ -478,8 +478,8 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF (CRef (Libnames.Ident (Loc.ghost,id1),None)) in let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty (CRef (Libnames.Ident (Loc.ghost,id2),None)) in - let f1type = Typing.type_of (Global.env()) Evd.empty f1 in - let f2type = Typing.type_of (Global.env()) Evd.empty f2 in + let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in + let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in let ar2 = List.length (fst (decompose_prod f2type)) in let _ = diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9e3f39863..065c12a2d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -487,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = The "value" of this branch is then simply [res] *) let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in - let rt_typ = Typing.type_of env Evd.empty rt_as_constr in + let rt_typ = Typing.unsafe_type_of env Evd.empty rt_as_constr in let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -595,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env Evd.empty v in - let v_type = Typing.type_of env Evd.empty v_as_constr in + let v_type = Typing.unsafe_type_of env Evd.empty v_as_constr in let new_env = match n with Anonymous -> env @@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> @@ -643,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = nal in let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> @@ -690,7 +690,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in - Typing.type_of env Evd.empty case_arg_as_constr + Typing.unsafe_type_of env Evd.empty case_arg_as_constr ) el in (****** The next works only if the match is not dependent ****) @@ -737,7 +737,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.fold_right (fun id acc -> let typ_of_id = - Typing.type_of env_with_pat_ids Evd.empty (mkVar id) + Typing.unsafe_type_of env_with_pat_ids Evd.empty (mkVar id) in let raw_typ_of_id = Detyping.detype false [] @@ -791,7 +791,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env Evd.empty (mkVar id) in let raw_typ_of_id = Detyping.detype false [] new_env Evd.empty typ_of_id in @@ -1105,7 +1105,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 t',ctx = Pretyping.understand env Evd.empty t in - let type_t' = Typing.type_of env Evd.empty t' in + let type_t' = Typing.unsafe_type_of env Evd.empty t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1255,7 +1255,7 @@ let do_build_inductive let evd,env = Array.fold_right2 (fun id c (evd,env) -> - let evd,t = Typing.e_type_of env evd (mkConstU c) in + let evd,t = Typing.type_of env evd (mkConstU c) in evd, Environ.push_named (id,None,t) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e211b6883..5dcb0c043 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -72,11 +72,11 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,NoBindings, Tacmach.pf_type_of g' princ,g') + (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError("",str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_type_of g princ,g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let princ_infos = Tactics.compute_elim_sig princ_type in let args_as_induction_constr = @@ -356,8 +356,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (fun i x -> let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in - let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in - let _ = evd := evd' in + let _ = evd := evd' in + let princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd uprinc in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d10924f88..89ceb751a 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -127,8 +127,8 @@ let generate_type evd g_to_f f graph i = let evd',graph = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph))) in - let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in evd:=evd'; + let graph_arity = Typing.e_type_of (Global.env ()) evd graph in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -193,7 +193,7 @@ let find_induction_principle evd f = | None -> raise Not_found | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in - let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in + let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -296,7 +296,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_type_of g (mkVar hid) in + let type_of_hid = pf_unsafe_type_of g (mkVar hid) in match kind_of_term type_of_hid with | Prod(_,_,t') -> begin @@ -440,7 +440,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes "functional_induction" ( (fun gl -> let term = mkApp (mkVar principle_id,Array.of_list bindings) in - let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true) gl term in + let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) @@ -577,7 +577,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match kind_of_term (pf_type_of g (mkVar id)) with + match kind_of_term (pf_unsafe_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g @@ -642,7 +642,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in let graph_principle = nf_zeta schemes.(i) in - let princ_type = pf_type_of g graph_principle in + let princ_type = pf_unsafe_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig princ_type in (* Then we get the number of argument of the function and compute a fresh name for each of them @@ -772,7 +772,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in + let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info @@ -900,7 +900,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing *) let revert_graph kn post_tac hid g = - let typ = pf_type_of g (mkVar hid) in + let typ = pf_unsafe_type_of g (mkVar hid) in match kind_of_term typ with | App(i,args) when isInd i -> let ((kn',num) as ind'),u = destInd i in @@ -951,7 +951,7 @@ let revert_graph kn post_tac hid g = let functional_inversion kn hid fconst f_correct : tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in - let type_of_h = pf_type_of g (mkVar hid) in + let type_of_h = pf_unsafe_type_of g (mkVar hid) in match kind_of_term type_of_h with | App(eq,args) when eq_constr eq (make_eq ()) -> let pre_tac,f_args,res = @@ -1003,7 +1003,7 @@ let invfun qhyp f g = Proofview.V82.of_tactic begin Tactics.try_intros_until (fun hid -> Proofview.V82.tactic begin fun g -> - let hyp_typ = pf_type_of g (mkVar hid) in + let hyp_typ = pf_unsafe_type_of g (mkVar hid) in match kind_of_term hyp_typ with | App(eq,args) when eq_constr eq (make_eq ()) -> begin diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 77a7f006b..b5a42b307 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,7 +115,7 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] - (pf_type_of gls c) + (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -400,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = thin to_intros; h_intros to_intros; (fun g' -> - let ty_teq = pf_type_of g' (mkVar heq) in + let ty_teq = pf_unsafe_type_of g' (mkVar heq) in let teq_lhs,teq_rhs = let _,args = try destApp ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -514,13 +514,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app (pf_type_of g (mkVar id)) with + match decompose_app (pf_unsafe_type_of g (mkVar id)) with | _, t::_ -> eq_constr t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) @@ -655,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} let pf_type c tac gl = - let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in + let evars, ty = Typing.type_of (pf_env gl) (project gl) c in tclTHEN (Refiner.tclEVARS evars) (tac ty) gl let pf_typel l tac = @@ -680,7 +680,7 @@ let mkDestructEq : if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in - let type_of_expr = pf_type_of g expr in + let type_of_expr = pf_unsafe_type_of g expr in let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 10cf21360..93588111b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1120,7 +1120,7 @@ struct with e when Errors.noncritical e -> (X(t),env,tg) in let is_prop term = - let ty = Typing.type_of (Goal.env gl) (Goal.sigma gl) term in + let ty = Typing.unsafe_type_of (Goal.env gl) (Goal.sigma gl) term in let sort = Typing.sort_of (Goal.env gl) (ref (Goal.sigma gl)) ty in Term.is_prop_sort sort in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4e2696dfd..710a2394d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1689,7 +1689,7 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.nf_enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in let rec loop = function diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 7844a36c1..f73a15dba 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *) let env = Global.env() and sigma = Evd.empty in fst (Constrintern.interp_constr env sigma c) -let ty c = Typing.type_of (Global.env()) Evd.empty c +let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c let decl_constant na ctx c = let vars = Universes.universes_of_constr c in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fcbe90b6a..ef196e0a7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1668,7 +1668,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.e_type_of extenv !evdref t in + let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in @@ -2014,7 +2014,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env - {uj_val = ty; uj_type = Typing.type_of env !evdref ty} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind; @@ -2214,7 +2214,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8ebb8cd27..f5135f5c6 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in (try subco () with NoSubtacCoercion -> - let typ = Typing.type_of env evm c in - let typ' = Typing.type_of env evm c' in + let typ = Typing.unsafe_type_of env evm c in + let typ' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm typ) then *) coerce_application typ typ' c c' l l') (* else subco () *) @@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | x, y when Constr.equal c c' -> if Int.equal (Array.length l) (Array.length l') then let evm = !evdref in - let lam_type = Typing.type_of env evm c in - let lam_type' = Typing.type_of env evm c' in + let lam_type = Typing.unsafe_type_of env evm c in + let lam_type' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm lam_type) then ( *) coerce_application lam_type lam_type' c c' l l' (* ) else subco () *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index e28180713..a0493777a 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -343,56 +343,49 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx next = +let authorized_occ env sigma partial_app closed pat c mk_ctx = try let subst = matches_core_closed env sigma false partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst) - then next () - else mkresult subst (mk_ctx (mkMeta special_meta)) next - with PatternMatchingFailure -> next () + then (fun next -> next ()) + else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let rec aux env c mk_ctx next = - match kind_of_term c with + let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let next () = match kind_of_term c with | Cast (c1,k,c2) -> let next_mk_ctx = function | [c1] -> mk_ctx (mkCast (c1, k, c2)) | _ -> assert false in - let next () = try_aux [env, c1] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux [env, c1] next_mk_ctx next | Lambda (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) | _ -> assert false in - let next () = - let env' = Environ.push_rel (x,None,c1) env in - try_aux [(env, c1); (env', c2)] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let env' = Environ.push_rel (x,None,c1) env in + try_aux [(env, c1); (env', c2)] next_mk_ctx next | Prod (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) | _ -> assert false in - let next () = - let env' = Environ.push_rel (x,None,c1) env in - try_aux [(env, c1); (env', c2)] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let env' = Environ.push_rel (x,None,c1) env in + try_aux [(env, c1); (env', c2)] next_mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in - let next () = - let env' = Environ.push_rel (x,Some c1,t) env in - try_aux [(env, c1); (env', c2)] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let env' = Environ.push_rel (x,Some c1,t) env in + try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let next () = let topdown = true in if partial_app then if topdown then @@ -421,45 +414,40 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in let sub = (env, c1) :: subargs env lc in try_aux sub mk_ctx next - in - authorized_occ env sigma partial_app closed pat c mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, hd) :: (env, c1) :: subargs env lc in - let next () = try_aux sub next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + let sub = (env, c1) :: (env, hd) :: subargs env lc in + try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in let sub = subargs env types @ subargs env bodies in - let next () = try_aux sub next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux sub next_mk_ctx next | CoFix (i,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in let sub = subargs env types @ subargs env bodies in - let next () = try_aux sub next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux sub next_mk_ctx next | Proj (p,c') -> let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - let next () = if partial_app then try let term = Retyping.expand_projection env sigma p c' [] in aux env term mk_ctx next with Retyping.RetypeError _ -> next () else - try_aux [env, c'] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next + try_aux [env, c'] next_mk_ctx next | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - authorized_occ env sigma partial_app closed pat c mk_ctx next + next () + in + here next (* Tries [sub_match] for all terms in the list *) and try_aux lc mk_ctx next = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2508f4ef3..ee6bbe7fb 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -713,7 +713,7 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = whd_evar evd evi.evar_concl in + let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = @@ -795,8 +795,10 @@ let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in + let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let sort = destSort concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s + Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index bd427ecd0..ac4e3b306 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -378,8 +378,8 @@ and nf_predicate env ind mip params v pT = | _, _ -> false, nf_type env v let native_norm env sigma c ty = - if !Flags.no_native_compiler then - error "Native_compute reduction has been disabled" + if Coq_config.no_native_compiler then + error "Native_compute reduction has been disabled at configure time." else let penv = Environ.pre_env env in (* diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0cadffa4f..03fe2122c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -374,7 +374,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.type_of env evd c in + let ty = Typing.unsafe_type_of env evd c in make_judge c ty let judge_of_Type evd s = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 372b26aa2..8a5db9059 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1134,7 +1134,7 @@ let abstract_scheme env (locc,a) (c, sigma) = let pattern_occs loccs_trm env sigma c = let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in try - let _ = Typing.type_of env sigma abstr_trm in + let _ = Typing.unsafe_type_of env sigma abstr_trm in sigma, applist(abstr_trm, List.map snd loccs_trm) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c6209cc33..fb5927dbf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -270,7 +270,7 @@ let check env evdref c t = (* Type of a constr *) -let type_of env evd c = +let unsafe_type_of env evd c = let j = execute env (ref evd) c in j.uj_type @@ -283,7 +283,7 @@ let sort_of env evdref c = (* Try to solve the existential variables by typing *) -let e_type_of ?(refresh=false) env evd c = +let type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) @@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type else !evdref, j.uj_type +let e_type_of ?(refresh=false) env evdref c = + let j = execute env evdref c in + (* side-effect on evdref *) + if refresh then + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in + let () = evdref := evd in + c + else j.uj_type + let solve_evars env evdref c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1f822f1a5..bfae46ff8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -13,12 +13,15 @@ open Evd (** This module provides the typing machine with existential variables and universes. *) -(** Typecheck a term and return its type *) -val type_of : env -> evar_map -> constr -> types +(** Typecheck a term and return its type. May trigger an evarmap leak. *) +val unsafe_type_of : env -> evar_map -> constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types +val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types + +(** Variant of [type_of] using references instead of state-passing. *) +val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) val sort_of : env -> evar_map ref -> types -> sorts diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c2281e13a..b5fe5d0b6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -93,7 +93,7 @@ let abstract_list_all env evd typ c l = let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in let evd,typp = - try Typing.e_type_of env evd p + try Typing.type_of env evd p with | UserError _ -> error_cannot_find_well_typed_abstraction env evd p l None @@ -1150,7 +1150,7 @@ let applyHead env evd n c = apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.type_of env evd c) evd + apprec n c (Typing.unsafe_type_of env evd c) evd let is_mimick_head ts f = match kind_of_term f with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2c9c695bf..a2cccc0e0 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -28,7 +28,7 @@ open Misctypes (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c (******************************************************************) (* Clausal environments *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 898588d9e..5c48995fc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -83,7 +83,7 @@ let apply_to_hyp sign id f = else sign let check_typability env sigma c = - if !check then let _ = type_of env sigma c in () + if !check then let _ = unsafe_type_of env sigma c in () (************************************************************************) (************************************************************************) @@ -317,7 +317,7 @@ let meta_free_prefix a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then type_of env sigma c + if !check then unsafe_type_of env sigma c else Retyping.get_type_of env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d25f7e915..f172bbdd1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -30,9 +30,13 @@ let cbv_vm env sigma c = Vnorm.cbv_vm env c ctyp let cbv_native env sigma c = - let ctyp = Retyping.get_type_of env sigma c in - let evars = Nativenorm.evars_of_evar_map sigma in - Nativenorm.native_norm env evars c ctyp + if Coq_config.no_native_compiler then + let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in + cbv_vm env sigma c + else + let ctyp = Retyping.get_type_of env sigma c in + let evars = Nativenorm.evars_of_evar_map sigma in + Nativenorm.native_norm env evars c ctyp let whd_cbn flags env sigma t = let (state,_) = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index fa0d03623..4238d1e37 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -84,6 +84,7 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -172,6 +173,9 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl + let pf_unsafe_type_of gl t = + pf_apply unsafe_type_of gl t + let pf_type_of gl t = pf_apply type_of gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f7fc6b54f..a0e1a0157 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,7 +41,8 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_type_of : goal sigma -> constr -> types +val pf_unsafe_type_of : goal sigma -> constr -> types +val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> named_declaration @@ -112,7 +113,8 @@ module New : sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_concl : [ `NF ] Proofview.Goal.t -> types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier diff --git a/stm/stm.ml b/stm/stm.ml index 977156475..97903e721 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -846,7 +846,8 @@ end = struct (* {{{ *) | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup") | Some vcs, _ -> vcs in let cb, _ = - Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in + try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) + with Failure _ -> raise Proof_global.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in diff --git a/tactics/auto.ml b/tactics/auto.ml index 7da841571..72ba9e0bd 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -377,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Extern tacast -> conclPattern concl p tacast in - tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic) + tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic) and trivial_resolve dbg mod_delta db_list local_db cl = try diff --git a/tactics/auto.mli b/tactics/auto.mli index 0cc8a0b1b..8dacc1362 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -19,7 +19,7 @@ val extern_interp : (** Auto and related automation tactics *) -val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list +val priority : ('a * full_hint) list -> ('a * full_hint) list val default_search_depth : int ref diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ad8164fa6..2b3fadf7f 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -263,7 +263,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) @@ -281,7 +281,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.type_of env sigma c in + let ctype = Typing.unsafe_type_of env sigma c in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3fafbe15a..e1fe51656 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -149,7 +149,7 @@ let e_give_exact flags poly (c,clenv) gl = c, {gl with sigma = clenv'.evd} else c, gl in - let t1 = pf_type_of gl c in + let t1 = pf_unsafe_type_of gl c in tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = @@ -168,7 +168,7 @@ let unify_resolve poly flags (c,clenv) gls = let clenv_of_prods poly nprods (c, clenv) gls = if poly || Int.equal nprods 0 then Some clenv else - let ty = pf_type_of gls c in + let ty = pf_unsafe_type_of gls c in let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) @@ -231,13 +231,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl = | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in + let tac = Proofview.V82.of_tactic (run_hint t tac) in let tac = if complete then tclCOMPLETE tac else tac in - match repr_auto_tactic t with - | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t)) + match repr_hint t with + | Extern _ -> (tac,b,true, name, lazy (pr_hint t)) | _ -> (* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) - (tac,b,false, name, lazy (pr_autotactic t)) + (tac,b,false, name, lazy (pr_hint t)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db sigma concl = @@ -842,6 +842,6 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_type_of gl c in + let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in unify_e_resolve false flags (c,ce) gl diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c03710e91..22f218b4f 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -90,7 +90,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.nf_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index bd55e6fb1..b7dc7b493 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -35,7 +35,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.nf_enter begin fun gl -> - let t1 = Tacmach.New.pf_type_of gl c in + let t1 = Tacmach.New.pf_unsafe_type_of gl c in let t2 = Tacmach.New.pf_concl gl in if occur_existential t1 || occur_existential t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) @@ -182,8 +182,8 @@ and e_my_find_search db_list local_db hdc concl = | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) | Extern tacast -> conclPattern concl p tacast in - let tac = run_auto_tactic t tac in - (tac, lazy (pr_autotactic t))) + let tac = run_hint t tac in + (tac, lazy (pr_hint t))) in List.map tac_of_hint hintl diff --git a/tactics/elim.ml b/tactics/elim.ml index 3cb4fa9c4..4841d2c25 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -85,7 +85,7 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = pf_type_of gl in + let type_of = pf_unsafe_type_of gl in let typc = type_of c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) @@ -139,7 +139,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.nf_enter begin fun gl -> - let idty = pf_type_of gl (mkVar id) in + let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 2ee4bf8e1..a5d68e19b 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -133,7 +133,7 @@ let match_eqdec c = let solveArg eqonleft op a1 a2 tac = Proofview.Goal.enter begin fun gl -> - let rectype = pf_type_of gl a1 in + let rectype = pf_unsafe_type_of gl a1 in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let subtacs = if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] @@ -203,7 +203,7 @@ let decideEquality rectype = let compare c1 c2 = Proofview.Goal.enter begin fun gl -> - let rectype = pf_type_of gl c1 in + let rectype = pf_unsafe_type_of gl c1 in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro diff --git a/tactics/equality.ml b/tactics/equality.ml index f2860a230..ea74dc37e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = - let ct = pf_type_of gl c in - let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in - let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in - [eqclause] + let sigma, ct = pf_type_of gl c in + let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in + let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in + [eqclause] let rewrite_conv_closed_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; @@ -944,7 +944,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.nf_enter begin fun gl -> - let type_of = pf_type_of gl in + let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in @@ -1019,7 +1019,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (dependent (mkRel lind) rty); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in - let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in + let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in let (na,_,_) = lookup_rel lind env in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in @@ -1053,7 +1053,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1099,7 +1099,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = type_of env sigma dflt in + let dflt_typ = unsafe_type_of env sigma dflt in try let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in @@ -1118,7 +1118,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (destEvar ev) with | Some w -> - let w_type = type_of env sigma w in + let w_type = unsafe_type_of env sigma w in if Evarconv.e_cumul env evdref w_type a then let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) @@ -1200,7 +1200,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1253,7 +1253,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in @@ -1293,7 +1293,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let injfun = mkNamedLambda e t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in - let sigma, pf_typ = Typing.e_type_of env sigma pf in + let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in let pf = Clenvtac.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in @@ -1460,8 +1460,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) let expected_goal = nf_betaiota sigma expected_goal in (* Retype to get universes right *) - let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in - let sigma, _ = Typing.e_type_of env sigma body in + let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in + let sigma, _ = Typing.type_of env sigma body in sigma,body,expected_goal (* Like "replace" but decompose dependent equalities *) @@ -1662,26 +1662,40 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } +let regular_subst_tactic = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "more regular behavior of tactic subst"; + optkey = ["Regular";"Subst";"Tactic"]; + optread = (fun () -> !regular_subst_tactic); + optwrite = (:=) regular_subst_tactic } + let subst_all ?(flags=default_subst_tactic_flags ()) () = + if !regular_subst_tactic then + (* First step: find hypotheses to treat in linear time *) let find_equations gl = let gl = Proofview.Goal.assume gl in + let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let test (hyp,_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if Term.eq_constr x y then None else match kind_of_term x, kind_of_term y with - | Var _, _ | _, Var _ -> Some hyp - | _ -> None + | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> + Some hyp + | _ -> + None with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in - List.map_filter test hyps + List.rev (List.map_filter test hyps) in (* Second step: treat equations *) @@ -1694,9 +1708,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with - | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true) - | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false) - | _ -> Proofview.tclUNIT () + | Var x', _ when not (occur_term x y) -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (occur_term y x) -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) + | _ -> + Proofview.tclUNIT () end in Proofview.Goal.nf_enter begin fun gl -> @@ -1704,6 +1721,30 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = tclMAP process ids end + else + +(* Old implementation, not able to manage configurations like a=b, a=t, + or situations like "a = S b, b = S a", or also accidentally unfolding + let-ins *) + Proofview.Goal.nf_enter begin fun gl -> + let find_eq_data_decompose = find_eq_data_decompose gl in + let test (_,c) = + try + let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + if flags.only_leibniz then restrict_to_eq_and_identity eq; + (* J.F.: added to prevent failure on goal containing x=x as an hyp *) + if Term.eq_constr x y then failwith "caught"; + match kind_of_term x with Var x -> x | _ -> + match kind_of_term y with Var y -> y | _ -> failwith "caught" + with Constr_matching.PatternMatchingFailure -> failwith "caught" in + let test p = try Some (test p) with Failure _ -> None in + let hyps = pf_hyps_types gl in + let ids = List.map_filter test hyps in + let ids = List.uniquize ids in + subst_gen flags.rewrite_dependent_proof ids + end + (* Rewrite the first assumption for which a condition holds and gives the direction of the rewrite *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f217cda89..177be2c20 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -704,7 +704,7 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); Proofview.Goal.nf_enter begin fun gl -> @@ -755,7 +755,7 @@ let destauto t = let destauto_in id = Proofview.Goal.nf_enter begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype diff --git a/tactics/hints.ml b/tactics/hints.ml index f83aa5601..0df1a35c6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -68,7 +68,7 @@ let decompose_app_bound t = (* The Type of Constructions Autotactic Hints *) (************************************************************************) -type 'a auto_tactic_ast = +type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -92,23 +92,64 @@ type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set -type 'a auto_tactic = 'a auto_tactic_ast +type 'a with_uid = { + obj : 'a; + uid : KerName.t; +} + +type hint = (constr * clausenv) hint_ast with_uid -type 'a gen_auto_tactic = { +type 'a with_metadata = { pri : int; (* A number lower is higher priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) name : hints_path_atom; (* A potential name to refer to the hint *) - code : 'a (* the tactic to apply when the concl matches pat *) + code : 'a; (* the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic +type full_hint = hint with_metadata type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic - -let run_auto_tactic tac k = k tac -let repr_auto_tactic tac = tac + (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata + +type import_level = [ `LAX | `WARN | `STRICT ] + +let warn_hint : import_level ref = ref `LAX +let read_warn_hint () = match !warn_hint with +| `LAX -> "Lax" +| `WARN -> "Warn" +| `STRICT -> "Strict" + +let write_warn_hint = function +| "Lax" -> warn_hint := `LAX +| "Warn" -> warn_hint := `WARN +| "Strict" -> warn_hint := `STRICT +| _ -> error "Only the following flags are accepted: Lax, Warn, Strict." + +let _ = + Goptions.declare_string_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "behavior of non-imported hints"; + Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; + Goptions.optread = read_warn_hint; + Goptions.optwrite = write_warn_hint; + } + +let fresh_key = + let id = Summary.ref ~name:"HINT-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) let eq_hints_path_atom p1 p2 = match p1, p2 with | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2 @@ -125,7 +166,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with | (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _ | Unfold_nth _ | Extern _), _ -> false -let eq_gen_auto_tactic t1 t2 = +let eq_hint_metadata t1 t2 = Int.equal t1.pri t2.pri && Option.equal constr_pattern_eq t1.pat t2.pat && eq_hints_path_atom t1.name t2.name && @@ -153,7 +194,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0 - un discrimination net borné (Btermdn.t) constitué de tous les patterns de la seconde liste de tactiques *) -type stored_data = int * pri_auto_tactic +type stored_data = int * full_hint (* First component is the index of insertion in the table, to keep most recent first semantics. *) module Bounded_net = Btermdn.Make(struct @@ -175,21 +216,7 @@ let empty_se = { sentry_mode = []; } -let eq_pri_auto_tactic (_, x) (_, y) = - if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then - match x.code,y.code with - | Res_pf (cstr,_),Res_pf (cstr1,_) -> - Term.eq_constr cstr cstr1 - | ERes_pf (cstr,_),ERes_pf (cstr1,_) -> - Term.eq_constr cstr cstr1 - | Give_exact (cstr,_),Give_exact (cstr1,_) -> - Term.eq_constr cstr cstr1 - | Res_pf_THEN_trivial_fail (cstr,_) - ,Res_pf_THEN_trivial_fail (cstr1,_) -> - Term.eq_constr cstr cstr1 - | _,_ -> false - else - false +let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid let add_tac pat t st se = match pat with @@ -248,7 +275,7 @@ let instantiate_hint p = { cl.templval with rebus = strip_params env cl.templval.rebus }; env = empty_env} in - let code = match p.code with + let code = match p.code.obj with | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx) | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx) | Res_pf_THEN_trivial_fail (c, cty, ctx) -> @@ -256,7 +283,8 @@ let instantiate_hint p = | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx) | Unfold_nth e -> Unfold_nth e | Extern t -> Extern t - in { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code } + in + { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with | PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 @@ -473,15 +501,14 @@ module Hint_db = struct let idv = id, v in let k = match gr with | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && - is_unfold v.code then None else Some gr + is_unfold v.code.obj then None else Some gr | None -> None in let dnst = if db.use_dn then Some db.hintdb_state else None in - let pat = if not db.use_dn && is_exact v.code then None else v.pat in + let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in match k with | None -> - (** ppedrot: this equality here is dubious. Maybe we can remove it? *) - let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in + let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in if not (List.exists is_present db.hintdb_nopat) then (** FIXME *) { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } @@ -500,7 +527,7 @@ module Hint_db = struct let add_one (k, v) db = let v = instantiate_hint v in let st',db,rebuild = - match v.code with + match v.code.obj with | Unfold_nth egr -> let addunf (ids,csts) (ids',csts') = match egr with @@ -586,6 +613,7 @@ let auto_init_db = Hintdbmap.empty) let searchtable : hint_db_table = ref auto_init_db +let statustable = ref KNmap.empty let searchtable_map name = Hintdbmap.find name !searchtable @@ -609,9 +637,10 @@ let add_hints_init f = let init = !hints_init in hints_init := (fun () -> init (); f ()) -let init () = searchtable := auto_init_db; !hints_init () -let freeze _ = !searchtable -let unfreeze fs = searchtable := fs +let init () = + searchtable := auto_init_db; statustable := KNmap.empty; !hints_init () +let freeze _ = (!searchtable, !statustable) +let unfreeze (fs, st) = searchtable := fs; statustable := st let _ = Summary.declare_summary "search" { Summary.freeze_function = freeze; @@ -632,6 +661,8 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable." +let with_uid c = { obj = c; uid = fresh_key () } + let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = let cty = strip_outer_cast cty in match kind_of_term cty with @@ -647,7 +678,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = poly = poly; pat = Some pat; name = name; - code = Give_exact (c, cty, ctx) }) + code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in @@ -667,7 +698,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; - code = Res_pf(c,cty,ctx) }) + code = with_uid (Res_pf(c,cty,ctx)); }) else begin if not eapply then failwith "make_apply_entry"; if verbose then @@ -678,7 +709,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; - code = ERes_pf(c,cty,ctx) }) + code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -724,7 +755,7 @@ let make_unfold eref = poly = false; pat = None; name = PathHints [g]; - code = Unfold_nth eref }) + code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = let hdconstr = Option.map try_head_pattern pat in @@ -733,7 +764,7 @@ let make_extern pri pat tacast = poly = false; pat = pat; name = PathAny; - code = Extern tacast }) + code = with_uid (Extern tacast) }) let make_mode ref m = let ty = Global.type_of_global_unsafe ref in @@ -749,14 +780,14 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (type_of env sigma c) in + let t = hnf_constr env sigma (unsafe_type_of env sigma c) in let hd = head_of_constr_reference (head_constr t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; - code=Res_pf_THEN_trivial_fail(c,t,ctx) }) + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -771,7 +802,15 @@ let get_db dbname = try searchtable_map dbname with Not_found -> Hint_db.empty empty_transparent_state false -let add_hint dbname hintlist = +let add_hint dbname hintlist = + let check (_, h) = + let () = if KNmap.mem h.code.uid !statustable then + error "Conflicting hint keys. This can happen when including \ + twice the same module." + in + statustable := KNmap.add h.code.uid false !statustable + in + let () = List.iter check hintlist in let db = get_db dbname in let db' = Hint_db.add_list hintlist db in searchtable_add (dbname,db') @@ -816,7 +855,7 @@ type hint_obj = { hint_action : hint_action; } -let cache_autohint (_, h) = +let load_autohint _ (kn, h) = let name = h.hint_name in match h.hint_action with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) @@ -826,6 +865,16 @@ let cache_autohint (_, h) = | AddCut path -> add_cut name path | AddMode (l, m) -> add_mode name l m +let open_autohint i (kn, h) = + if Int.equal i 1 then match h.hint_action with + | AddHints hints -> + let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in + List.iter add hints + | _ -> () + +let cache_autohint (kn, obj) = + load_autohint 1 (kn, obj); open_autohint 1 (kn, obj) + let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in @@ -837,34 +886,36 @@ let subst_autohint (subst, obj) = let subst_hint (k,data as hint) = let k' = Option.smartmap subst_key k in let pat' = Option.smartmap (subst_pattern subst) data.pat in - let code' = match data.code with + let code' = match data.code.obj with | Res_pf (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'==t then data.code else Res_pf (c', t',ctx) + if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx) | ERes_pf (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'==t then data.code else ERes_pf (c',t',ctx) + if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx) | Give_exact (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'== t then data.code else Give_exact (c',t',ctx) + if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx) | Res_pf_THEN_trivial_fail (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx) + if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx) | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in - if ref==ref' then data.code else Unfold_nth ref' + if ref==ref' then data.code.obj else Unfold_nth ref' | Extern tac -> let tac' = Tacsubst.subst_tactic subst tac in - if tac==tac' then data.code else Extern tac' + if tac==tac' then data.code.obj else Extern tac' in let name' = subst_path_atom subst data.name in + let uid' = subst_kn subst data.code.uid in let data' = - if data.pat==pat' && data.name == name' && data.code==code' then data - else { data with pat = pat'; name = name'; code = code' } + if data.code.uid == uid' && data.pat == pat' && + data.name == name' && data.code.obj == code' then data + else { data with pat = pat'; name = name'; code = { obj = code'; uid = uid' } } in if k' == k && data' == data then hint else (k',data') in @@ -896,7 +947,8 @@ let classify_autohint obj = let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; - load_function = (fun _ -> cache_autohint); + load_function = load_autohint; + open_function = open_autohint; subst_function = subst_autohint; classify_function = classify_autohint; } @@ -1146,8 +1198,7 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_autotactic = - function +let pr_hint h = match h.obj with | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c) | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c) | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c) @@ -1163,11 +1214,11 @@ let pr_autotactic = in (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) -let pr_hint (id, v) = - (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) +let pr_id_hint (id, v) = + (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) let pr_hint_list hintlist = - (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ()) + (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) let pr_hints_db (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ @@ -1266,3 +1317,27 @@ let pr_searchtable () = in Hintdbmap.fold fold !searchtable (mt ()) +let print_mp mp = + try + let qid = Nametab.shortest_qualid_of_module mp in + str " from " ++ pr_qualid qid + with Not_found -> mt () + +let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true + +let warn h x = + let hint = pr_hint h in + let (mp, _, _) = KerName.repr h.uid in + let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in + Proofview.tclUNIT x + +let run_hint tac k = match !warn_hint with +| `LAX -> k tac.obj +| `WARN -> + if is_imported tac then k tac.obj + else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x) +| `STRICT -> + if is_imported tac then k tac.obj + else Proofview.tclZERO (UserError ("", (str "Tactic failure."))) + +let repr_hint h = h.obj diff --git a/tactics/hints.mli b/tactics/hints.mli index 958cca1c3..687bc78c7 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array (** Pre-created hint databases *) -type 'a auto_tactic_ast = +type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -36,13 +36,13 @@ type 'a auto_tactic_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) -type 'a auto_tactic +type hint type hints_path_atom = | PathHints of global_reference list | PathAny -type 'a gen_auto_tactic = private { +type 'a with_metadata = private { pri : int; (** A number between 0 and 4, 4 = lower priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) @@ -50,7 +50,7 @@ type 'a gen_auto_tactic = private { code : 'a; (** the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic +type full_hint = hint with_metadata type search_entry @@ -76,28 +76,28 @@ module Hint_db : type t val empty : transparent_state -> bool -> t val find : global_reference -> t -> search_entry - val map_none : t -> pri_auto_tactic list + val map_none : t -> full_hint list (** All hints associated to the reference *) - val map_all : global_reference -> t -> pri_auto_tactic list + val map_all : global_reference -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) - val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) - val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list + val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list val add_one : hint_entry -> t -> t val add_list : (hint_entry) list -> t -> t val remove_one : global_reference -> t -> t val remove_list : global_reference list -> t -> t - val iter : (global_reference option -> bool array list -> pri_auto_tactic list -> unit) -> t -> unit + val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state @@ -197,12 +197,12 @@ val make_extern : int -> constr_pattern option -> Tacexpr.glob_tactic_expr -> hint_entry -val run_auto_tactic : 'a auto_tactic -> - ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic +val run_hint : hint -> + ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic (** This function is for backward compatibility only, not to use in newly written code. *) -val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast +val repr_hint : hint -> (constr * clausenv) hint_ast val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t @@ -227,7 +227,7 @@ val pr_applicable_hint : unit -> std_ppcmds val pr_hint_ref : global_reference -> std_ppcmds val pr_hint_db_by_name : hint_db_name -> std_ppcmds val pr_hint_db : Hint_db.t -> std_ppcmds -val pr_autotactic : (constr * 'a) auto_tactic -> Pp.std_ppcmds +val pr_hint : hint -> Pp.std_ppcmds (** Hook for changing the initialization of auto *) diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4b94f420b..95f3af57e 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -411,7 +411,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_type_of gl e1 in (t,e1,e2) + let t = pf_unsafe_type_of gl e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if pf_conv_x gl t1 t2 then (t1,e1,e2) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5502356fb..ef115aea0 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl = let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args @@ -437,7 +437,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in Errors.errorlabstrm "" msg diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 60ce0e0dc..6d26e91c6 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -226,6 +226,7 @@ end) = struct let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> + let b = Reductionops.nf_betaiota (goalevars evars) b in if noccurn 1 b (* non-dependent product *) then let ty = Reductionops.nf_betaiota (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in @@ -380,7 +381,7 @@ end let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in - let evd', t = Typing.e_type_of env (goalevars evars) c in + let evd', t = Typing.type_of env (goalevars evars) c in (evd', cstrevars evars), c module PropGlobal = struct @@ -452,7 +453,6 @@ let convertible env evd x y = Reductionops.is_conv_leq env evd x y type hypinfo = { - env : env; prf : constr; car : constr; rel : constr; @@ -472,7 +472,7 @@ let rec decompose_app_rel env evd t = | App (f, [||]) -> assert false | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in - let ty = Typing.type_of env evd argl in + let ty = Typing.unsafe_type_of env evd argl in let f'' = mkLambda (Name default_dependent_ident, ty, mkLambda (Name (Id.of_string "y"), lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) @@ -498,7 +498,7 @@ let decompose_applied_relation env sigma (c,l) = let sort = sort_of_rel env sigma equiv in let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in let value = mkApp (c, args) in - Some (sigma, { env=env; prf=value; + Some (sigma, { prf=value; car=ty1; rel = equiv; sort = Sorts.is_prop sort; c1=c1; c2=c2; holes }) in @@ -510,10 +510,6 @@ let decompose_applied_relation env sigma (c,l) = | Some c -> c | None -> error "Cannot find an homogeneous relation to rewrite." -let decompose_applied_relation_expr env sigma (is, (c,l)) = - let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in - decompose_applied_relation env sigma cbl - let rewrite_db = "rewrite" let conv_transparent_state = (Id.Pred.empty, Cpred.full) @@ -588,24 +584,12 @@ let general_rewrite_unif_flags () = Unification.resolve_evars = true } -let refresh_hypinfo env sigma hypinfo c = - let sigma, hypinfo = match hypinfo with - | None -> - decompose_applied_relation_expr env sigma c - | Some hypinfo -> - if hypinfo.env != env then - (* If the lemma actually generates existential variables, we cannot - use it here as it will polute the evar map with existential variables - that might not ever get instantiated (e.g. if we rewrite under a - binder and need to refresh [c] again) *) - (* TODO: remove bindings in sigma corresponding to c *) - decompose_applied_relation_expr env sigma c - else sigma, hypinfo - in +let refresh_hypinfo env sigma (is, cb) = + let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma cb in + let sigma, hypinfo = decompose_applied_relation env sigma cbl in let { c1; c2; car; rel; prf; sort; holes } = hypinfo in sigma, (car, rel, prf, c1, c2, holes, sort) - (** FIXME: write this in the new monad interface *) let solve_remaining_by env sigma holes by = match by with @@ -719,7 +703,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = let rew_prf = RewPrf (rel, prf) in let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in let rew = if l2r then rew else symmetry env sort rew in - Some ((), rew) + Some rew with | e when Class_tactics.catchable e -> None | Reduction.NotConvertible -> None @@ -763,7 +747,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in - let appmtype = Typing.type_of env (goalevars evars) appm in + let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -829,27 +813,27 @@ let coerce env avoid cstr res = let rel, prf = get_rew_prf res in apply_constraint env avoid res.rew_car rel prf cstr res -let apply_rule unify loccs : ('a * int) pure_strategy = +let apply_rule unify loccs : int pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in let is_occ occ = if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in - fun (hypinfo, occ) env avoid t ty cstr evars -> - let unif = if isEvar t then None else unify hypinfo env evars t in + fun occ env avoid t ty cstr evars -> + let unif = if isEvar t then None else unify env evars t in match unif with - | None -> ((hypinfo, occ), Fail) - | Some (hypinfo', rew) -> + | None -> (occ, Fail) + | Some rew -> let occ = succ occ in - if not (is_occ occ) then ((hypinfo, occ), Fail) - else if eq_constr t rew.rew_to then ((hypinfo, occ), Identity) + if not (is_occ occ) then (occ, Fail) + else if eq_constr t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in let rel, prf = get_rew_prf res in let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in - ((hypinfo', occ), res) - + (occ, res) + let apply_lemma l2r flags oc by loccs : strategy = fun () env avoid t ty cstr (sigma, cstrs) -> let sigma, c = oc sigma in @@ -857,13 +841,13 @@ let apply_lemma l2r flags oc by loccs : strategy = let { c1; c2; car; rel; prf; sort; holes } = hypinfo in let rew = (car, rel, prf, c1, c2, holes, sort) in let evars = (sigma, cstrs) in - let unify () env evars t = + let unify env evars t = let rew = unify_eqn rew l2r flags env evars by t in match rew with | None -> None - | Some rew -> Some ((), rew) + | Some rew -> Some rew in - let _, res = apply_rule unify loccs ((), 0) env avoid t ty cstr evars in + let _, res = apply_rule unify loccs 0 env avoid t ty cstr evars in (), res let e_app_poly env evars f args = @@ -1379,11 +1363,10 @@ end let rewrite_with l2r flags c occs : strategy = fun () env avoid t ty cstr (sigma, cstrs) -> - let hypinfo = None in - let unify hypinfo env evars t = + let unify env evars t = let (sigma, cstrs) = evars in let ans = - try Some (refresh_hypinfo env sigma hypinfo c) + try Some (refresh_hypinfo env sigma c) with e when Class_tactics.catchable e -> None in match ans with @@ -1392,14 +1375,14 @@ let rewrite_with l2r flags c occs : strategy = let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in match rew with | None -> None - | Some rew -> Some (None, rew) (** reset the hypinfo cache *) + | Some rew -> Some rew in let app = apply_rule unify occs in let strat = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in - let _, res = strat (hypinfo, 0) env avoid t ty cstr (sigma, cstrs) in + let _, res = strat 0 env avoid t ty cstr (sigma, cstrs) in ((), res) let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars = @@ -1755,7 +1738,7 @@ let declare_projection n instance_id r = let poly = Global.is_polymorphic r in let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in let term = proper_projection c ty in - let typ = Typing.type_of (Global.env ()) Evd.empty term in + let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1788,7 +1771,7 @@ let build_morphism_signature m = let env = Global.env () in let m,ctx = Constrintern.interp_constr env Evd.empty m in let sigma = Evd.from_env ~ctx env in - let t = Typing.type_of env sigma m in + let t = Typing.unsafe_type_of env sigma m in let cstrs = let rec aux t = match kind_of_term t with @@ -1815,7 +1798,7 @@ let build_morphism_signature m = let default_morphism sign m = let env = Global.env () in - let t = Typing.type_of env Evd.empty m in + let t = Typing.unsafe_type_of env Evd.empty m in let evars, _, sign, cstrs = PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -1967,12 +1950,12 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in - let unify () env evars t = unify_abs res l2r sort env evars t in + let unify env evars t = unify_abs res l2r sort env evars t in let app = apply_rule unify occs in let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in let substrat = Strategies.fix recstrat in let strat () env avoid t ty cstr evars = - let _, res = substrat ((), 0) env avoid t ty cstr evars in + let _, res = substrat 0 env avoid t ty cstr evars in (), res in let origsigma = project gl in @@ -2011,7 +1994,7 @@ let setoid_proof ty fn fallback = try let rel, _, _ = decompose_app_rel env sigma concl in let evm = sigma in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in + let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in (try init_setoid () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e @@ -2070,7 +2053,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = Proofview.V82.tactic (fun gl -> - let ctype = pf_type_of gl (mkVar id) in + let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum ctype in let (equiv, args) = decompose_app concl in let rec split_last_two = function diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index cae00f5a8..40a18ac45 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -55,10 +55,7 @@ type rewrite_result = | Identity | Success of rewrite_result_info -type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types -> - (bool (* prop *) * constr option) -> evars -> 'a * rewrite_result - -type strategy = unit pure_strategy +type strategy val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index e8cb8c63b..492b51f1a 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -26,6 +26,8 @@ let interp_alias key = try KNmap.find key !alias_map with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) +let check_alias key = KNmap.mem key !alias_map + (** ML tactic extensions (TacML) *) type ml_tactic = diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 424bb142c..7ee591cca 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit val interp_alias : alias -> glob_tactic_expr (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +val check_alias : alias -> bool +(** Returns [true] if an alias is defined, false otherwise. *) + (** {5 Coq tactic definitions} *) val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7ce158fd1..374c7c736 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -734,7 +734,7 @@ let interp_may_eval f ist env sigma = function str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.e_type_of ~refresh:true env sigma c_interp + Typing.type_of ~refresh:true env sigma c_interp | ConstrTerm c -> try f ist env sigma c diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5ba53a764..7d1cc3341 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -598,7 +598,7 @@ module New = struct (** FIXME: evar leak. *) let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -651,7 +651,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3038a9506..2791d7c48 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -158,7 +158,7 @@ let convert_concl ?(check=true) ty k = Proofview.Refine.refine ~unsafe:true begin fun sigma -> let sigma = if check then begin - ignore (Typing.type_of env sigma ty); + ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; sigma @@ -628,7 +628,7 @@ let change_on_subterm cv_pb deep t where env sigma c = env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.type_of env sigma c) + try ignore (Typing.unsafe_type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; @@ -979,7 +979,7 @@ let cut c = let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) - let typ = Typing.type_of env sigma c in + let typ = Typing.unsafe_type_of env sigma c in let typ = whd_betadeltaiota env sigma typ in match kind_of_term typ with | Sort _ -> true @@ -1224,7 +1224,7 @@ let find_ind_eliminator ind s gl = evd, c let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in + let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); @@ -1639,7 +1639,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter begin fun gl -> - match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with + match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in @@ -1672,7 +1672,7 @@ let exact_check c = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, ct = Typing.e_type_of env sigma c in + let sigma, ct = Typing.type_of env sigma c in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end @@ -1821,7 +1821,7 @@ let specialize (c,lbind) g = let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else - let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in + let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -1841,11 +1841,11 @@ let specialize (c,lbind) g = | Var id when Id.List.mem id (pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST - (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g) (exact_no_check term)) g | _ -> tclTHEN tac (tclTHENLAST - (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g) (exact_no_check term)) g (* Keeping only a few hypotheses *) @@ -1980,7 +1980,7 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> @@ -1994,7 +1994,7 @@ let intro_decomp_eq loc l thin tac id = let intro_or_and_pattern loc bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let nv = constructors_nrealargs ind in let ll = fix_empty_or_and_pattern (Array.length nv) ll in @@ -2013,7 +2013,7 @@ let rewrite_hyp assert_style l2r id = let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in let t = whd_betadeltaiota (type_of (mkVar id)) in match match_with_equality_type t with @@ -2290,7 +2290,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in - let sigma, _ = Typing.e_type_of env sigma term in + let sigma, _ = Typing.type_of env sigma term in sigma, term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) @@ -2376,7 +2376,7 @@ let forward b usetac ipat c = match usetac with | None -> Proofview.Goal.enter begin fun gl -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c)) end @@ -2459,7 +2459,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = mkProd_or_LetIn (na,b,t) cl', evd' let generalize_goal gl i ((occs,c,b),na as o) cl = - let t = pf_type_of gl c in + let t = pf_unsafe_type_of gl c in let env = pf_env gl in generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl @@ -2520,7 +2520,7 @@ let new_generalize_gen_let lconstr = let (newcl, sigma), args = List.fold_right_i (fun i ((_,c,b),_ as o) (cl, args) -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let args = if Option.is_empty b then c :: args else args in generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) @@ -2797,7 +2797,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match kind_of_term c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN @@ -3201,7 +3201,7 @@ let abstract_args gl generalize_vars dep id defined f args = let rel, c = Reductionops.splay_prod_n env sigma 1 prod in List.hd rel, c in - let argty = pf_type_of gl arg in + let argty = pf_unsafe_type_of gl arg in let ty = (* refresh_universes_strict *) ty in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3242,7 +3242,7 @@ let abstract_args gl generalize_vars dep id defined f args = in if dogen then let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -3566,13 +3566,13 @@ let guess_elim isrec dep s hyp0 gl = Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s else Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in - let elimt = Tacmach.New.pf_type_of gl elimc in + let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess + Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = (Id.t list * (elim_arg_kind * bool * Id.t) list) array @@ -3604,7 +3604,7 @@ let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = - let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in + let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -3963,7 +3963,7 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4225,7 +4225,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE begin @@ -4276,7 +4276,7 @@ let prove_transitivity hdcncl eq_kind t = | HeterogenousEq (typ1,c1,typ2,c2) -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let type_of = Typing.type_of env sigma in + let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index ef991365d..f85a60264 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -1,3 +1,5 @@ +(* Check that the subterms of the predicate of a match are taken into account *) + Require Import List. Open Scope list_scope. Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), @@ -11,3 +13,25 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), match goal with | [ |- appcontext G[@hd] ] => idtac end. + +(* This second example comes from CFGV where inspecting subterms of a + match is expecting to inspect first the term to match (even though + it would certainly be better to provide a "match x with _ end" + construct for generically matching a "match") *) + +Ltac find_head_of_head_match T := + match T with context [?E] => + match T with + | E => fail 1 + | _ => constr:(E) + end + end. + +Ltac mydestruct := + match goal with + | |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E + end. + +Goal forall x, match x with 0 => 0 | _ => 0 end = 0. +intros. +mydestruct. diff --git a/test-suite/bugs/closed/4216.v b/test-suite/bugs/closed/4216.v new file mode 100644 index 000000000..ae7f74677 --- /dev/null +++ b/test-suite/bugs/closed/4216.v @@ -0,0 +1,20 @@ +Generalizable Variables T A. + +Inductive path `(a: A): A -> Type := idpath: path a a. + +Class TMonad (T: Type -> Type) := { + bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B; + ret: forall {A: Type}, A -> T A; + ret_unit_left: forall {A B: Type} (k: A -> T B) (a: A), + path (bind (ret a) k) (k a) + }. + +Let T_fzip `{TMonad T} := fun (A B: Type) (f: T (A -> B)) (t: T A) + => bind t (fun a => bind f (fun g => ret (g a) )). +Let T_pure `{TMonad T} := @ret _ _. + +Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A): + path (T_fzip A A (T_pure (A -> A) t) x) x. + unfold T_fzip, T_pure. + Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)). + diff --git a/test-suite/bugs/closed/4232.v b/test-suite/bugs/closed/4232.v new file mode 100644 index 000000000..61e544a91 --- /dev/null +++ b/test-suite/bugs/closed/4232.v @@ -0,0 +1,20 @@ +Require Import Setoid Morphisms Vector. + +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Global Declare Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n). +Global Declare Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n). + +Global Declare Instance tl_proper1 {A} `{Equiv A} n: + Proper ((equiv) ==> (equiv)) + (@tl A n). + +Lemma test: + forall {A} `{Setoid A} n (xa ya: Vector.t A (S n)), + (equiv xa ya) -> equiv (tl xa) (tl ya). +Proof. + intros A R HA n xa ya Heq. + setoid_rewrite Heq. + reflexivity. +Qed. diff --git a/test-suite/bugs/closed/4234.v b/test-suite/bugs/closed/4234.v new file mode 100644 index 000000000..348dd49d9 --- /dev/null +++ b/test-suite/bugs/closed/4234.v @@ -0,0 +1,7 @@ +Definition UU := Type. + +Definition dirprodpair {X Y : UU} := existT (fun x : X => Y). + +Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }. +Proof. + refine (dirprodpair _ (fun x => _)). diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/opened/4214.v index cd53c898e..3daf45213 100644 --- a/test-suite/bugs/closed/4214.v +++ b/test-suite/bugs/opened/4214.v @@ -2,4 +2,4 @@ Goal forall A (a b c : A), b = a -> b = c -> a = c. intros. subst. -reflexivity. +Fail reflexivity. diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v new file mode 100644 index 000000000..7215bd990 --- /dev/null +++ b/test-suite/success/extraction_polyprop.v @@ -0,0 +1,11 @@ +(* The current extraction cannot handle this situation, + and shouldn't try, otherwise it might produce some Ocaml + code that segfaults. See Table.error_singleton_become_prop + or S. Glondu's thesis for more details. *) + +Definition f {X} (p : (nat -> X) * True) : X * nat := + (fst p 0, 0). + +Definition f_prop := f ((fun _ => I),I). + +Fail Extraction f_prop. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1a40e5d59..15cb02d37 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -89,6 +89,11 @@ Section Defs. Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 := { }. + (** An Equivalence is a PreOrder plus symmetry. *) + + Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 := + { }. + (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) := diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c34bbd56e..2437184a9 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -45,8 +45,8 @@ Section Lists. Definition hd_error (l:list A) := match l with - | [] => error - | x :: _ => value x + | [] => None + | x :: _ => Some x end. Definition tl (l:list A) := @@ -393,11 +393,11 @@ Section Elts. simpl; auto. Qed. - Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A := + Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A := match n, l with - | O, x :: _ => value x + | O, x :: _ => Some x | S n, _ :: l => nth_error l n - | _, _ => error + | _, _ => None end. Definition nth_default (default:A) (l:list A) (n:nat) : A := diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 11b4b3732..36d29a1e8 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -575,8 +575,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other let decl_var var = function |[] -> () |l -> - printf "%s:=" var; print_list "\\\n " l; print "\n"; - printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var + printf "%s:=" var; print_list "\\\n " l; print "\n\n"; + print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "else\nifeq ($(MAKECMDGOALS),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "endif\nendif\n\n"; + printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var in section "Files dispatching."; decl_var "VFILES" vfiles; diff --git a/tools/coqc.ml b/tools/coqc.ml index 7e822dbe3..aed229abc 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -109,7 +109,7 @@ let parse_args () = |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" - |"-impredicative-set"|"-vm"|"-no-native-compiler" + |"-impredicative-set"|"-vm"|"-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" |"-indices-matter"|"-quick"|"-color"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" @@ -122,7 +122,7 @@ let parse_args () = |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" - |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w" as o) :: rem -> begin match rem with diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 96bb89e2a..f90508090 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -355,7 +355,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = ) in Proofview.Goal.nf_enter begin fun gl -> - let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = try @@ -417,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let tt1 = Tacmach.New.pf_type_of gl t1 in + let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 diff --git a/toplevel/class.ml b/toplevel/class.ml index 6a485d52c..0e270f960 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly = let _ = if not (Reductionops.is_conv_leq env Evd.empty - (Typing.type_of env Evd.empty val_f) typ_f) + (Typing.unsafe_type_of env Evd.empty val_f) typ_f) then errorlabstrm "" (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/toplevel/command.ml b/toplevel/command.ml index 1249581ee..7cf0477f9 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -847,7 +847,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in - let relty = Typing.type_of env !evdref rel in + let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = user_err_loc (constr_loc r, @@ -988,7 +988,7 @@ let interp_recursive isfix fixl notations = List.fold_left2 (fun env' id t -> if Flags.is_program_mode () then - let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in + let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ca379cb7e..56b544292 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -114,6 +114,11 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type () let set_batch_mode () = batch_mode := true +let set_warning = function +| "all" -> make_warn true +| "none" -> make_warn false +| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1 + let toplevel_default_name = DirPath.make [Id.of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) let set_toplevel_name dir = @@ -276,7 +281,16 @@ let print_style_tags () = in print_string opt in - List.iter iter tags; + let make (t, st) = match st with + | None -> None + | Some st -> + let tags = List.map string_of_int (Terminal.repr st) in + let t = String.concat "." (Ppstyle.repr t) in + Some (t ^ "=" ^ String.concat ";" tags) + in + let repr = List.map_filter make tags in + let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in + let () = List.iter iter tags in flush_all () let error_missing_arg s = @@ -472,6 +486,7 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo |"-toploop" -> toploop := Some (next ()) + |"-w" -> set_warning (next ()) (* Options with zero arg *) |"-async-queries-always-delegate" @@ -498,11 +513,14 @@ let parse_args arglist = |"-noinit"|"-nois" -> load_init := false |"-no-compat-notations" -> no_compat_ntn := true |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-no-native-compiler" -> no_native_compiler := true + |"-native-compiler" -> + if Coq_config.no_native_compiler then + warning "Native compilation was disabled at configure time." + else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-q" -> no_load_rc () - |"-quiet"|"-silent" -> Flags.make_silent true + |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index deffb4fe5..98b322af1 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -84,8 +84,14 @@ type tactic_grammar_obj = { tacobj_body : Tacexpr.glob_tactic_expr } +let check_key key = + if Tacenv.check_alias key then + error "Conflicting tactic notations keys. This can happen when including \ + twice the same module." + let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in + let () = check_key key in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp @@ -97,6 +103,7 @@ let open_tactic_notation i (_, tobj) = let load_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in + let () = check_key key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f053839c7..50fb019f4 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -56,6 +56,10 @@ let print_usage_channel co command = \n -v print Coq version and exit\ \n -list-tags print highlight color tags known by Coq and exit\ \n\ +\n -quiet unset display of extra information (implies -w none)\ +\n -w (all|none) configure display of warnings\ +\n -color (on|off|auto) configure color output (only active through coqtop)\ +\n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ \n -batch batch mode (exits just after arguments parsing)\ @@ -63,7 +67,6 @@ let print_usage_channel co command = \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ \n -emacs tells Coq it is executed under Emacs\ -\n -color (on|off|auto) configure color output (only active through coqtop)\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ @@ -71,7 +74,7 @@ let print_usage_channel co command = \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ \n -time display the time taken by each command\ -\n -no-native-compiler disable the native_compute reduction machinery\ +\n -native-compiler precompile files for the native_compute machinery\ \n -h, -help print this list of options\ \n"; List.iter (fun (name, text) -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 11cb047e0..5418c60e9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -78,9 +78,13 @@ let get_exn_files e = Exninfo.get e files_of_exn let add_exn_files e f = Exninfo.add e files_of_exn f -let raise_with_file f (e, info) = - let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in - iraise (e, add_exn_files info { outer = f; inner = inner_f }) +let enrich_with_file f (e, info) = + let inner = match get_exn_files info with None -> f | Some x -> x.inner in + (e, add_exn_files info { outer = f; inner }) + +let raise_with_file f e = iraise (enrich_with_file f e) + +let cur_file = ref None let disable_drop = function | Drop -> Errors.error "Drop is forbidden." @@ -253,13 +257,12 @@ let rec vernac_com verbosely checknav (loc,com) = else iraise (reraise, info) and read_vernac_file verbosely s = - Flags.make_warn verbosely; let checknav loc cmd = if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" in - let (in_chan, fname, input) = - open_file_twice_if verbosely s in + let (in_chan, fname, input) = open_file_twice_if verbosely s in + cur_file := Some fname; try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) @@ -350,3 +353,8 @@ let compile v f = compile v f; CoqworkmgrApi.giveback 1 +let () = Hook.set Stm.process_error_hook (fun e -> + match !cur_file with + | None -> Cerrors.process_vernac_interp_error e + | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e) +) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4300d5e24..9d5edc80a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -379,17 +379,27 @@ let msg_found_library = function msg_info (hov 0 (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) -let err_unmapped_library loc qid = +let err_unmapped_library loc ?from qid = let dir = fst (repr_qualid qid) in + let prefix = match from with + | None -> str "." + | Some from -> + str " and prefix " ++ pr_dirpath from ++ str "." + in user_err_loc (loc,"locate_library", - strbrk "Cannot find a physical path bound to logical path " ++ - pr_dirpath dir ++ str".") + strbrk "Cannot find a physical path bound to logical path matching suffix " ++ + pr_dirpath dir ++ prefix) -let err_notfound_library loc qid = +let err_notfound_library loc ?from qid = + let prefix = match from with + | None -> str "." + | Some from -> + str " with prefix " ++ pr_dirpath from ++ str "." + in user_err_loc (loc,"locate_library", - strbrk "Unable to locate library " ++ pr_qualid qid ++ str".") + strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -759,8 +769,8 @@ let vernac_require from import qidl = let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library loc qid - | Library.LibNotFound -> err_notfound_library loc qid + | Library.LibUnmappedDir -> err_unmapped_library loc ?from:root qid + | Library.LibNotFound -> err_notfound_library loc ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then @@ -2164,5 +2174,4 @@ let interp ?(verbosely=true) ?proof (loc,c) = else aux false c let () = Hook.set Stm.interp_hook interp -let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error let () = Hook.set Stm.with_fail_hook with_fail |