diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 22 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 17 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 9 | ||||
| -rw-r--r-- | kernel/term.ml | 28 | ||||
| -rw-r--r-- | kernel/term.mli | 31 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | lib/future.mli | 4 | ||||
| -rw-r--r-- | lib/pp.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 244 | ||||
| -rw-r--r-- | pretyping/cases.ml | 5 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 23 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 6 | ||||
| -rw-r--r-- | stm/stm.ml | 4 | ||||
| -rw-r--r-- | tactics/auto.ml | 16 | ||||
| -rw-r--r-- | tactics/auto.mli | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 42 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 24 | ||||
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4325.v | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4372.v | 20 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 26 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
27 files changed, 222 insertions, 350 deletions
@@ -5,6 +5,9 @@ Vernacular commands - New command "Redirect" to redirect the output of a command to a file. - New command "Undelimit Scope" to remove the delimiter of a scope. +- New option "Strict Universe Declaration", set by default. It enforces the + declaration of all polymorphic universes appearing in a definition when + introducing it. Tactics diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index bea25a92f..2f07beb72 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -367,7 +367,8 @@ There is a for loop that repeats a tactic {\num} times: \begin{quote} {\tt do} {\num} {\tacexpr} \end{quote} -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +{\tacexpr} is evaluated to $v$ which must be a tactic value. +This tactic value $v$ is applied {\num} times. Supposing ${\num}>1$, after the first application of $v$, $v$ is applied, at least once, to the generated subgoals and so on. It fails if the application of $v$ fails before @@ -394,7 +395,8 @@ We can catch the tactic errors with: \begin{quote} {\tt try} {\tacexpr} \end{quote} -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +{\tacexpr} is evaluated to $v$ which must be a tactic value. +The tactic value $v$ is applied to each focused goal independently. If the application of $v$ fails in a goal, it catches the error and leaves the goal unchanged. If the level of the exception is positive, then the @@ -406,7 +408,8 @@ We can check if a tactic made progress with: \begin{quote} {\tt progress} {\tacexpr} \end{quote} -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +{\tacexpr} is evaluated to $v$ which must be a tactic value. +The tactic value $v$ is applied to each focued subgoal independently. If the application of $v$ to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 @@ -422,7 +425,7 @@ We can branch with the following structure: {\tacexpr}$_1$ {\tt +} {\tacexpr}$_2$ \end{quote} {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and -$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied to each +$v_2$ which must be tactic values. The tactic value $v_1$ is applied to each focused goal independently and if it fails or a later tactic fails, then the proof backtracks to the current goal and $v_2$ is applied. @@ -462,7 +465,7 @@ Yet another way of branching without backtracking is the following structure: {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ \end{quote} {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and -$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied in each +$v_2$ which must be tactic values. The tactic value $v_1$ is applied in each subgoal independently and if it fails \emph{to progress} then $v_2$ is applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress} @@ -494,7 +497,8 @@ single success \emph{a posteriori}: \begin{quote} {\tt once} {\tacexpr} \end{quote} -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +{\tacexpr} is evaluated to $v$ which must be a tactic value. +The tactic value $v$ is applied but only its first success is used. If $v$ fails, {\tt once} {\tacexpr} fails like $v$. If $v$ has a least one success, {\tt once} {\tacexpr} succeeds once, but cannot produce more successes. @@ -505,7 +509,8 @@ Coq provides an experimental way to check that a tactic has \emph{exactly one} s \begin{quote} {\tt exactly\_once} {\tacexpr} \end{quote} -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +{\tacexpr} is evaluated to $v$ which must be a tactic value. +The tactic value $v$ is applied if it has at most one success. If $v$ fails, {\tt exactly\_once} {\tacexpr} fails like $v$. If $v$ has a exactly one success, {\tt exactly\_once} {\tacexpr} succeeds like $v$. If $v$ has @@ -592,7 +597,8 @@ amount of time: \begin{quote} {\tt timeout} {\num} {\tacexpr} \end{quote} -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +{\tacexpr} is evaluated to $v$ which must be a tactic value. +The tactic value $v$ is applied normally, except that it is interrupted after ${\num}$ seconds if it is still running. In this case the outcome is a failure. diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 47a5510b0..75134e6f1 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -94,14 +94,6 @@ struct let print_char = fun c -> (); fun () -> print_char c - (** {!Pp.pp}. The buffer is also flushed. *) - let print_debug = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> - let (e, info) = Errors.push e in raise ~info e () - - (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.msg_notice s; Pp.pp_flush () with e -> - let (e, info) = Errors.push e in raise ~info e () - let timeout = fun n t -> (); fun () -> Control.timeout n t (Exception Timeout) @@ -111,6 +103,13 @@ struct let (e, info) = Errors.push e in Util.iraise (Exception e, info) + (** Use the current logger. The buffer is also flushed. *) + let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) + let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) + let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) + let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) + let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) + let run = fun x -> try x () with Exception e as src -> let (src, info) = Errors.push src in @@ -155,7 +154,7 @@ struct shape of the monadic type is reminiscent of that of the continuation monad transformer. - The paper also contains the rational for the [split] abstraction. + The paper also contains the rationale for the [split] abstraction. An explanation of how to derive such a monad from mathematical principles can be found in "Kan Extensions for Program diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 35dd311a8..42a84f830 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -55,12 +55,13 @@ module NonLogical : sig val read_line : string t val print_char : char -> unit t - (** {!Pp.pp}. The buffer is also flushed. *) - val print : Pp.std_ppcmds -> unit t - (* FIXME: shouldn't we have a logger instead? *) - (** {!Pp.pp}. The buffer is also flushed. *) + (** Loggers. The buffer is also flushed. *) val print_debug : Pp.std_ppcmds -> unit t + val print_warning : Pp.std_ppcmds -> unit t + val print_notice : Pp.std_ppcmds -> unit t + val print_info : Pp.std_ppcmds -> unit t + val print_error : Pp.std_ppcmds -> unit t (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) diff --git a/kernel/term.ml b/kernel/term.ml index 7bf4c8182..33ed25fe1 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -566,8 +566,10 @@ let decompose_lam_assum = in lamdec_rec empty_rel_context -(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T - into the pair ([(xn,Tn);...;(x1,T1)],T) *) +(* Given a positive integer n, decompose a product or let-in term + of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair + of the quantifying context [(xn,None,Tn);..;(xi,Some + ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *) let decompose_prod_n_assum n = if n < 0 then error "decompose_prod_n_assum: integer parameter must be positive"; @@ -581,10 +583,12 @@ let decompose_prod_n_assum n = in prodec_rec empty_rel_context n -(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T - into the pair ([(xn,Tn);...;(x1,T1)],T) +(* Given a positive integer n, decompose a lambda or let-in term [fun + (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted + context [(xn,None,Tn);...;(xi,Some ci,Ti);...;(x1,None,T1)] and of + the inner body [T]. Lets in between are not expanded but turn into local definitions, - but n is the actual number of destructurated lambdas. *) + but n is the actual number of destructurated lambdas. *) let decompose_lam_n_assum n = if n < 0 then error "decompose_lam_n_assum: integer parameter must be positive"; @@ -598,6 +602,20 @@ let decompose_lam_n_assum n = in lamdec_rec empty_rel_context n +(* Same, counting let-in *) +let decompose_lam_n_decls n = + if n < 0 then + error "decompose_lam_n_decls: integer parameter must be positive"; + let rec lamdec_rec l n c = + if Int.equal n 0 then l,c + else match kind_of_term c with + | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c + | Cast (c,_,_) -> lamdec_rec l n c + | c -> error "decompose_lam_n_decls: not enough abstractions" + in + lamdec_rec empty_rel_context n + (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction * gives n (casts are ignored) *) let nb_lam = diff --git a/kernel/term.mli b/kernel/term.mli index f8badb0dd..2bb811060 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -281,13 +281,15 @@ val decompose_prod : constr -> (Name.t*constr) list * constr {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *) val decompose_lam : constr -> (Name.t*constr) list * constr -(** Given a positive integer n, transforms a product term +(** Given a positive integer n, decompose a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} - into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *) + into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. + Raise a user error if not enough products. *) val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr -(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term - {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *) +(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term + {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}. + Raise a user error if not enough lambdas. *) val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form @@ -297,10 +299,15 @@ val decompose_prod_assum : types -> rel_context * types (** Idem with lambda's *) val decompose_lam_assum : constr -> rel_context * constr -(** Idem but extract the first [n] premisses *) +(** Idem but extract the first [n] premisses, counting let-ins. *) val decompose_prod_n_assum : int -> types -> rel_context * types + +(** Idem for lambdas, _not_ counting let-ins *) val decompose_lam_n_assum : int -> constr -> rel_context * constr +(** Idem, counting let-ins *) +val decompose_lam_n_decls : int -> constr -> rel_context * constr + (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) val nb_lam : constr -> int @@ -308,12 +315,14 @@ val nb_lam : constr -> int (** Similar to [nb_lam], but gives the number of products instead *) val nb_prod : constr -> int -(** Returns the premisses/parameters of a type/term (let-in included) *) +(** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context -(** Returns the first n-th premisses/parameters of a type/term (let included)*) +(** Return the first n-th premisses/parameters of a type (let included and counted) *) val prod_n_assum : int -> types -> rel_context + +(** Return the first n-th premisses/parameters of a term (let included but not counted) *) val lam_n_assum : int -> constr -> rel_context (** Remove the premisses/parameters of a type/term *) @@ -328,11 +337,11 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** flattens application lists *) +(** Flattens application lists *) val collapse_appl : constr -> constr -(** Removes recursively the casts around a term i.e. +(** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : constr -> constr @@ -352,10 +361,10 @@ type arity = rel_context * sorts (** Build an "arity" from its canonical form *) val mkArity : arity -> types -(** Destructs an "arity" into its canonical form *) +(** Destruct an "arity" into its canonical form *) val destArity : types -> arity -(** Tells if a term has the form of an arity *) +(** Tell if a term has the form of an arity *) val isArity : types -> bool (** {5 Kind of type} *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 09299f31d..4f32fdce8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -477,7 +477,7 @@ let rec execute env cstr = let j' = execute env1 c3 in judge_of_letin env name j1 j2 j' - | Cast (c,k, t) -> + | Cast (c,k,t) -> let cj = execute env c in let tj = execute_type env t in judge_of_cast env cj k tj diff --git a/lib/future.mli b/lib/future.mli index de2282ae9..adc15e49c 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation * When a future enters the environment a corresponding hook is run to perform * some work. If this fails, then its failure has to be annotated with the * same state id that corresponds to the future computation end. I.e. Qed - * is split into two parts, the lazy one (the future) and the eagher one + * is split into two parts, the lazy one (the future) and the eager one * (the hook), both performing some computations for the same state id. *) val fix_exn_of : 'a computation -> fix_exn (* Run remotely, returns the function to assign. If not blocking (the default) it raises NotReady if forced before the - delage assigns it. *) + delegate assigns it. *) type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] val create_delegate : ?blocking:bool -> name:string -> @@ -362,11 +362,11 @@ let emacs_quote_info_start = "<infomsg>" let emacs_quote_info_end = "</infomsg>" let emacs_quote g = - if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end + if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) else hov 0 g let emacs_quote_info g = - if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end + if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) else hov 0 g diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e7732a503..045beb37c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -247,247 +247,3 @@ END VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY ["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ] END - - - - - -(* FINDUCTION *) - -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" - (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) -let prNamedConstr s c = - begin - msg(str ""); - msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); - msg(str ""); - end - - - -(** Information about an occurrence of a function call (application) - inside a term. *) -type fapp_info = { - fname: constr; (** The function applied *) - largs: constr list; (** List of arguments *) - free: bool; (** [true] if all arguments are debruijn free *) - max_rel: int; (** max debruijn index in the funcall *) - onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) -} - - -(** [constr_head_match(a b c) a] returns true, false otherwise. *) -let constr_head_match u t= - if isApp u - then - let uhd,args= destApp u in - Constr.equal uhd t - else false - -(** [hdMatchSub inu t] returns the list of occurrences of [t] in - [inu]. DeBruijn are not pushed, so some of them may be unbound in - the result. *) -let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = - let subres = - match kind_of_term inu with - | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> - hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test - | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) - Array.fold_left - (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) - [] bl - | _ -> (* Cofix will be wrong *) - fold_constr - (fun l cstr -> - l @ hdMatchSub cstr test) [] inu in - if not (test inu) then subres - else - let f,args = decompose_app inu in - let freeset = Termops.free_rels inu in - let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in - {fname = f; largs = args; free = Int.Set.is_empty freeset; - max_rel = max_rel; onlyvars = List.for_all isVar args } - ::subres - -let make_eq () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) - -let mkEq typ c1 c2 = - mkApp (make_eq(),[| typ; c1; c2|]) - - -let poseq_unsafe idunsafe cstr gl = - 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 - (Proofview.V82.of_tactic (Tactics.assert_before Anonymous (mkEq typ (mkVar idunsafe) cstr))) - (Proofview.V82.of_tactic Tactics.reflexivity)) - gl - - -let poseq id cstr gl = - let x = Tactics.fresh_id [] id gl in - poseq_unsafe x cstr gl - -(* dirty? *) - -let list_constr_largs = ref [] - -let rec poseq_list_ids_rec lcstr gl = - match lcstr with - | [] -> tclIDTAC gl - | c::lcstr' -> - match kind_of_term c with - | Var _ -> - (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) - | _ -> - let _ = prstr "c = " in - let _ = prconstr c in - let _ = prstr "\n" 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 - let _ = prstr " list_constr_largs = " in - let _ = prlistconstr !list_constr_largs in - let _ = prstr "\n" in - - tclTHEN - (poseq_unsafe x c) - (poseq_list_ids_rec lcstr') - gl - -let poseq_list_ids lcstr gl = - let _ = list_constr_largs := [] in - poseq_list_ids_rec lcstr gl - -(** [find_fapp test g] returns the list of [app_info] of all calls to - functions that satisfy [test] in the conclusion of goal g. Trivial - repetition (not modulo conversion) are deleted. *) -let find_fapp (test:constr -> bool) g : fapp_info list = - let pre_res = hdMatchSub (Tacmach.pf_concl g) test in - let res = - List.fold_right (List.add_set Pervasives.(=)) pre_res [] in - (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); - res) - - - -(** [finduction id filter g] tries to apply functional induction on - an occurrence of function [id] in the conclusion of goal [g]. If - [id]=[None] then calls to any function are selected. In any case - [heuristic] is used to select the most pertinent occurrence. *) -let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) - (nexttac:Proof_type.tactic) g = - let test = match oid with - | Some id -> - let idref = const_of_id id in - (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *) - let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in - (fun u -> constr_head_match u idconstr) (* select only id *) - | None -> (fun u -> isApp u) in (* select calls to any function *) - let info_list = find_fapp test g in - let ordered_info_list = heuristic info_list in - prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); - if List.is_empty ordered_info_list then Errors.error "function not found in goal\n"; - let taclist: Proof_type.tactic list = - List.map - (fun info -> - (tclTHEN - (tclTHEN (poseq_list_ids info.largs) - ( - fun gl -> - (functional_induction - true (applist (info.fname, List.rev !list_constr_largs)) - None None) gl)) - nexttac)) ordered_info_list in - (* we try each (f t u v) until one does not fail *) - (* TODO: try also to mix functional schemes *) - tclFIRST taclist g - - - - -(** [chose_heuristic oi x] returns the heuristic for reordering - (and/or forgetting some elts of) a list of occurrences of - function calls infos to chose first with functional induction. *) -let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = - match oi with - | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) - | None -> - (* Default heuristic: put first occurrences where all arguments - are *bound* (meaning already introduced) variables *) - let ordering x y = - if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) - else if x.free && x.onlyvars then -1 - else if y.free && y.onlyvars then 1 - else 0 (* both not pertinent *) - in - List.sort ordering - - - -TACTIC EXTEND finduction - ["finduction" ident(id) natural_opt(oi)] -> - [ - match oi with - | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0" - | _ -> - let heuristic = chose_heuristic oi in - Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC) - ] -END - - - -TACTIC EXTEND fauto - [ "fauto" tactic(tac)] -> - [ - let heuristic = chose_heuristic None in - Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac))) - ] - | - [ "fauto" ] -> - [ - let heuristic = chose_heuristic None in - Proofview.V82.tactic (finduction None heuristic tclIDTAC) - ] - -END - - -TACTIC EXTEND poseq - [ "poseq" ident(x) constr(c) ] -> - [ Proofview.V82.tactic (poseq x c) ] -END - -VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY - [ "showindinfo" ident(x) ] -> [ Merge.showind x ] -END - -VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF - [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" - "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> - [ - let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty - (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.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 _ = - if not (Int.equal ar1 (List.length cl1)) then - Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in - let _ = - if not (Int.equal ar2 (List.length cl2)) then - Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in - Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id - ] -END diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 47d92f5e0..a5a7ace22 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1077,7 +1077,7 @@ let rec ungeneralize n ng body = let p = prod_applist p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in mkCase (ci,p,c,Array.map2 (fun q c -> - let sign,b = decompose_lam_n_assum q c in + let sign,b = decompose_lam_n_decls q c in it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign) ci.ci_cstr_ndecls brs) | App (f,args) -> @@ -1102,7 +1102,8 @@ let rec is_dependent_generalization ng body = | Case (ci,p,c,brs) -> (* We traverse a split *) Array.exists2 (fun q c -> - let _,b = decompose_lam_n_assum q c in is_dependent_generalization ng b) + let _,b = decompose_lam_n_decls q c in + is_dependent_generalization ng b) ci.ci_cstr_ndecls brs | App (g,args) -> (* We traverse an inner generalization *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 121ab7488..3fa037ffd 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -267,8 +267,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> - let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in - let ctx_b2',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in + let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in + let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in let n = rel_context_length ctx_b2 in let n' = rel_context_length ctx_b2' in if noccur_between 1 n b2 && noccur_between 1 n' b2' then @@ -413,12 +413,25 @@ 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 - | Case (ci,hd,c1,lc) -> + | Case (ci,p,c,brs) -> + (* Warning: this assumes predicate and branches to be + in canonical form using let and fun of the signature *) + let nardecls = List.length ci.ci_pp_info.ind_tags in + let sign_p,p = decompose_lam_n_decls (nardecls + 1) p in + let env_p = Environ.push_rel_context sign_p env in + let brs = Array.map2 decompose_lam_n_decls ci.ci_cstr_ndecls brs in + let sign_brs = Array.map fst brs in + let f (sign,br) = (Environ.push_rel_context sign env, br) in + let sub_br = Array.map f brs in let next_mk_ctx = function - | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + | c :: p :: brs -> + let p = it_mkLambda_or_LetIn p sign_p in + let brs = + Array.map2 it_mkLambda_or_LetIn (Array.of_list brs) sign_brs in + mk_ctx (mkCase (ci,p,c,brs)) | _ -> assert false in - let sub = (env, c1) :: (env, hd) :: subargs env lc in + let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a1213e72b..b5228094a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -302,7 +302,7 @@ and contract_branch isgoal e (cdn,can,mkpat,b) = let is_nondep_branch c l = try (* FIXME: do better using tags from l *) - let sign,ccl = decompose_lam_n_assum (List.length l) c in + let sign,ccl = decompose_lam_n_decls (List.length l) c in noccur_between 1 (rel_context_length sign) ccl with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false @@ -513,7 +513,7 @@ let rec detype flags avoid env sigma t = id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (Array.map_to_list (fun c -> (Id.of_string "A",c)) cl) + (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (dl,id, List.map (on_snd (detype flags avoid env sigma)) l) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a11c7b4e0..929bb86e8 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -97,7 +97,7 @@ val start_dependent_proof : val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. - * Both access the current proof state. The formes is supposed to be + * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 667765dbf..6d6215c52 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -33,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt()) let explain_logic_error_no_anomaly = ref (fun e -> mt()) let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) -let msg_tac_notice s = Proofview.NonLogical.print (s++fnl()) +let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) (* Prints the goal *) @@ -122,7 +122,7 @@ let run ini = let open Proofview.NonLogical in if not ini then begin - Proofview.NonLogical.print (str"\b\r\b\r") >> + Proofview.NonLogical.print_notice (str"\b\r\b\r") >> !skipped >>= fun skipped -> msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl()) end >> @@ -137,7 +137,7 @@ let rec prompt level = let runtrue = run true in begin let open Proofview.NonLogical in - Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with diff --git a/stm/stm.ml b/stm/stm.ml index ea31e0410..7dc0ff84a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -639,7 +639,7 @@ end = struct (* {{{ *) proof, Summary.project_summary (States.summary_of_state system) summary_pstate - let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) + let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable) let is_cached ?(cache=`No) id = if Stateid.equal id !cur_id then @@ -1912,7 +1912,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline "Initialising workers"; + prerr_endline "Initializing workers"; Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] diff --git a/tactics/auto.ml b/tactics/auto.ml index 9ca6162a2..dc4ac55b2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -72,16 +72,14 @@ let auto_flags_of_state st = (* Try unification with the precompiled clause, then use registered Apply *) -let unify_resolve poly flags ((c : raw_hint), clenv) = - Proofview.Goal.nf_enter begin fun gl -> +let connect_hint_clenv poly (c, _, ctx) clenv gl = (** [clenv] has been generated by a hint-making function, so the only relevant data in its evarmap is the set of metas. The [evar_reset_evd] function below just replaces the metas of sigma by those coming from the clenv. *) let sigma = Proofview.Goal.sigma gl in let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in (** Still, we need to update the universes *) - let (_, _, ctx) = c in - let clenv = + let clenv, c = if poly then (** Refresh the instance of the hint *) let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in @@ -91,11 +89,15 @@ let unify_resolve poly flags ((c : raw_hint), clenv) = (** FIXME: We're being inefficient here because we substitute the whole evar map instead of just its metas, which are the only ones mentioning the old universes. *) - Clenv.map_clenv map clenv + Clenv.map_clenv map clenv, map c else let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - { clenv with evd = evd ; env = Proofview.Goal.env gl } - in + { clenv with evd = evd ; env = Proofview.Goal.env gl }, c + in clenv, c + +let unify_resolve poly flags ((c : raw_hint), clenv) = + Proofview.Goal.nf_enter begin fun gl -> + let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in Clenvtac.clenv_refine false clenv end diff --git a/tactics/auto.mli b/tactics/auto.mli index 6e2acf7f5..cae180ce7 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -25,6 +25,9 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags +val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> + [ `NF ] Proofview.Goal.t -> clausenv * constr + (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c30957a67..83b1202b7 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -167,33 +167,31 @@ let e_give_exact flags poly (c,clenv) gl = tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = connect_clenv gls clenv' in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls + let clenv', c = connect_hint_clenv poly c clenv gls in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in + Clenvtac.clenv_refine true ~with_classes:false clenv' let unify_resolve poly flags (c,clenv) gls = - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = connect_clenv gls clenv' in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - Proofview.V82.of_tactic - (Clenvtac.clenv_refine false ~with_classes:false clenv') gls + let clenv', _ = connect_hint_clenv poly c clenv gls in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in + Clenvtac.clenv_refine false ~with_classes:false clenv' -let clenv_of_prods poly nprods (c, clenv) gls = +let clenv_of_prods poly nprods (c, clenv) gl = let (c, _, _) = c in if poly || Int.equal nprods 0 then Some clenv else - let ty = pf_unsafe_type_of gls c in + let ty = Tacmach.New.pf_unsafe_type_of gl c in let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) - Some (mk_clenv_from_n gls (Some diff) (c,ty)) + Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) else None -let with_prods nprods poly (c, clenv) f gls = - match clenv_of_prods poly nprods (c, clenv) gls with - | None -> tclFAIL 0 (str"Not enough premisses") gls - | Some clenv' -> f (c, clenv') gls +let with_prods nprods poly (c, clenv) f = + Proofview.Goal.nf_enter (fun gl -> + match clenv_of_prods poly nprods (c, clenv) gl with + | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") + | Some clenv' -> f (c, clenv') gl) (** Hack to properly solve dependent evars that are typeclasses *) @@ -237,12 +235,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl = let tac_of_hint = fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> let tac = function - | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags)) - | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) + | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags) + | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags) | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) | Res_pf_THEN_trivial_fail (term,cl) -> - Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) - (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) + Proofview.V82.tactic (tclTHEN + (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags)))) + (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) | Extern tacast -> conclPattern concl p tacast in @@ -902,4 +901,5 @@ let autoapply c i gl = (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) 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 + let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in + Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 1a84161e4..d0fd4b078 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -124,15 +124,17 @@ open Unification (***************************************************************************) let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) - -let unify_e_resolve poly flags (c,clenv) gls = - let (c, _, _) = c in - let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv - else clenv, Univ.empty_level_subst in - let clenv' = connect_clenv gls clenv' in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls + +let unify_e_resolve poly flags (c,clenv) = + Proofview.Goal.nf_enter begin + fun gl -> + let clenv', c = connect_hint_clenv poly c clenv gl in + Proofview.V82.tactic + (fun gls -> + let clenv' = clenv_unique_resolver ~flags clenv' gls in + tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls) + end let hintmap_of hdc concl = match hdc with @@ -176,10 +178,10 @@ and e_my_find_search db_list local_db hdc concl = (b, let tac = function | Res_pf (term,cl) -> unify_resolve poly st (term,cl) - | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl)) + | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> - Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_e_resolve poly st (term,cl))) + Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) | Extern tacast -> conclPattern concl p tacast diff --git a/tactics/equality.ml b/tactics/equality.ml index c6d74525f..740a165f8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1130,7 +1130,14 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." - | None -> anomaly (Pp.str "Not enough components to build the dependent tuple") + | None -> + (* This at least happens if what has been detected as a + dependency is not one; use an evasive error message; + even if the problem is upwards: unification should be + tried in the first place in make_iterated_tuple instead + of approximatively computing the free rels; then + unsolved evars would mean not binding rel *) + error "Cannot solve a unification problem." in let scf = sigrec_clausal_form siglen ty in !evdref, Evarutil.nf_evar !evdref scf diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ec6f04133..895064951 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -45,8 +45,8 @@ open Proofview.Notations let safe_msgnl s = Proofview.NonLogical.catch - (Proofview.NonLogical.print (s++fnl())) - (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) + (Proofview.NonLogical.print_debug (s++fnl())) + (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) type value = tlevel generic_argument @@ -1151,7 +1151,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with interp_message ist s >>= fun msg -> return (hov 0 msg , hov 0 msg) in - let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in + let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in let log (msg,_) = Proofview.Trace.log (fun () -> msg) in let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in Ftactic.run msgnl begin fun msgnl -> diff --git a/test-suite/bugs/closed/4325.v b/test-suite/bugs/closed/4325.v new file mode 100644 index 000000000..af69ca04b --- /dev/null +++ b/test-suite/bugs/closed/4325.v @@ -0,0 +1,5 @@ +Goal (forall a b : nat, Set = (a = b)) -> Set. +Proof. + clear. + intro H. + erewrite (fun H' => H _ H'). diff --git a/test-suite/bugs/closed/4372.v b/test-suite/bugs/closed/4372.v new file mode 100644 index 000000000..428192a34 --- /dev/null +++ b/test-suite/bugs/closed/4372.v @@ -0,0 +1,20 @@ +(* Tactic inversion was raising an anomaly because of a fake + dependency of TypeDenote into its argument *) + +Inductive expr := +| ETrue. + +Inductive IntermediateType : Set := ITbool. + +Definition TypeDenote (IT : IntermediateType) : Type := + match IT with + | _ => bool + end. + +Inductive ValueDenote : forall (e:expr) it, TypeDenote it -> Prop := +| VT : ValueDenote ETrue ITbool true. + +Goal forall it v, @ValueDenote ETrue it v -> True. + intros it v H. + inversion H. +Abort. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 6c4d4ae98..5bef2e512 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,29 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* Check that matching "match" does not look into the invisible + canonically generated binders of the return clause and of the branches *) + +Goal forall n, match n with 0 => true | S _ => false end = true. +intros. unfold nat_rect. +Fail match goal with |- context [nat] => idtac end. +Abort. + +(* Check that branches of automatically generated elimination + principle are correctly eta-expanded and hence matchable as seen + from the user point of view *) + +Goal forall a f n, nat_rect (fun _ => nat) a f n = 0. +intros. unfold nat_rect. +match goal with |- context [f _] => idtac end. +Abort. + +(* Check that branches of automatically generated elimination + principle are in correct form also in the presence of let-ins *) + +Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a. +Goal forall x, match x with c => 0 end = 1. +intros. +match goal with |- context [0] => idtac end. +Abort. diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 356ccdcc6..670447452 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -8,7 +8,7 @@ (** The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input - state, load the files given on the command line, load the ressource file, + state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) val init_toplevel : string list -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5344909b6..85d342bc4 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -478,7 +478,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = Some (snd (interp_redexp env evc r)) in do_definition id (local,p,k) pl bl red_option c typ_opt hook) -let vernac_start_proof p kind l lettop = +let vernac_start_proof locality p kind l lettop = + let local = enforce_locality_exp locality None in if Dumpglob.dump () then List.iter (fun (id, _) -> match id with @@ -488,7 +489,7 @@ let vernac_start_proof p kind l lettop = if lettop then errorlabstrm "Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); - start_proof_and_print (Global, p, Proof kind) l no_hook + start_proof_and_print (local, p, Proof kind) l no_hook let qed_display_script = ref true @@ -1860,7 +1861,7 @@ let interp ?proof ~loc locality poly c = (* Gallina *) | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d - | VernacStartTheoremProof (k,l,top) -> vernac_start_proof poly k l top + | VernacStartTheoremProof (k,l,top) -> vernac_start_proof locality poly k l top | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl @@ -1965,7 +1966,7 @@ let interp ?proof ~loc locality poly c = | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm") (* Proof management *) - | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false + | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () @@ -2006,7 +2007,7 @@ let check_vernac_supports_locality c l = | VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ - | VernacAssumption _ + | VernacAssumption _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ | VernacDeclareMLModule _ |