diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 53 |
1 files changed, 33 insertions, 20 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f29680e1..355745d9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,8 +44,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 @@ -557,7 +557,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; } in - intern_gen kind ~allow_patvar ~ltacvars env c + let kind_for_intern = + match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in + intern_gen kind_for_intern ~allow_patvar ~ltacvars env c in let trace = push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in @@ -678,7 +680,19 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let p = match a with - | Inl b -> Inl (interp_evaluable ist env sigma b) + | Inl (ArgVar (loc,id)) -> + (* This is the encoding of an ltac var supposed to be bound + prioritary to an evaluable reference and otherwise to a constr + (it is an encoding to satisfy the "union" type given to Simpl) *) + let coerce_eval_ref_or_constr x = + try Inl (coerce_to_evaluable_ref env x) + with CannotCoerceTo _ -> + let c = coerce_to_closed_constr env x in + Inr (pi3 (pattern_of_constr env sigma c)) in + (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) + with Not_found -> + error_global_not_found_loc loc (qualid_of_ident id)) + | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in interp_occurrences ist occs, p @@ -734,7 +748,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 @@ -971,10 +985,10 @@ let interp_induction_arg ist gl arg = let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl then keep,ElimOnIdent (loc,id') - else - (try keep,ElimOnConstr (fun env sigma -> sigma,(constr_of_id env id',NoBindings)) + else keep, ElimOnConstr (fun env sigma -> + try sigma, (constr_of_id env id', NoBindings) with Not_found -> - user_err_loc (loc,"", + user_err_loc (loc, "interp_induction_arg", pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")) in try @@ -1026,11 +1040,12 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt (* Reads a pattern by substituting vars of lfun *) let use_types = false -let eval_pattern lfun ist env sigma (_,pat as c) = +let eval_pattern lfun ist env sigma ((glob,_),pat as c) = + let bound_names = bound_glob_vars glob in if use_types then - pi3 (interp_typed_pattern ist env sigma c) + (bound_names,pi3 (interp_typed_pattern ist env sigma c)) else - instantiate_pattern env sigma lfun pat + (bound_names,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) @@ -1040,8 +1055,8 @@ let read_pattern lfun ist env sigma = function let cons_and_check_name id l = if Id.List.mem id l then user_err_loc (dloc,"read_match_goal_hyps", - strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^ - " used twice in the same pattern.")) + str "Hypothesis pattern-matching variable " ++ pr_id id ++ + str " used twice in the same pattern.") else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function @@ -1123,7 +1138,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 -> @@ -1492,11 +1507,11 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in catch_error_tac trace tac - | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected.")) + | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in eval_tactic ist tac - else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic.")) + else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.") (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist llc u = @@ -1752,10 +1767,8 @@ and interp_ltac_constr ist e : constr Ftactic.t = Ftactic.return cresult with CannotCoerceTo _ -> let env = Proofview.Goal.env gl in - Proofview.tclZERO (UserError ( "", - errorlabstrm "" - (str "Must evaluate to a closed term" ++ fnl() ++ - str "offending expression: " ++ fnl() ++ pr_inspect env e result))) + Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ + str "offending expression: " ++ fnl() ++ pr_inspect env e result) end |