diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7eff2b69fe..aa36074d2b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1175,7 +1175,8 @@ let solvable_by_tactic env evi (ev,args) src = Environ.named_context_of_val evi.evar_hyps = Environ.named_context env -> let id = id_of_string "H" in - start_proof id IsLocal evi.evar_hyps evi.evar_concl (fun _ _ -> ()); + start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl + (fun _ _ -> ()); begin try by (tclCOMPLETE tac); @@ -1520,7 +1521,7 @@ and interp_letin ist gl = function try let t = tactic_of_value v in let ndc = Environ.named_context_val env in - start_proof id IsLocal ndc typ (fun _ _ -> ()); + start_proof id (Local,Proof Lemma) ndc typ (fun _ _ -> ()); by t; let (_,({const_entry_body = pft},_,_)) = cook_proof () in delete_proof (dummy_loc,id); |