diff options
| author | herbelin | 2002-06-06 14:34:22 +0000 |
|---|---|---|
| committer | herbelin | 2002-06-06 14:34:22 +0000 |
| commit | 77b37b73d711af9b0725f1d63f99ad3157486cbb (patch) | |
| tree | 42a70ea4afe462a672ce5b7a2d9df23acc65b280 | |
| parent | 8639dd62e5bb477a9f52b8d1d2042796ae9f6233 (diff) | |
Ajout coercion constr vers hyp quantifiée
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e0a573d642..9609bb49f9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1047,11 +1047,8 @@ let interp_quantified_hypothesis ist = function | AnonHyp n -> AnonHyp n | NamedHyp id -> match eval_ident ist id with - | VIdentifier id -> NamedHyp id | VInteger n -> AnonHyp n - | _ -> invalid_arg_loc - (loc, "Not a reference to an hypothesis: "^(string_of_id id)) - + | v -> NamedHyp (coerce_to_hypothesis ist v) let interp_induction_arg ist = function | ElimOnConstr c -> ElimOnConstr (constr_interp ist c) @@ -1389,7 +1386,8 @@ and vcontext_interp ist = function | (VContext (ist',lr,lmr)) as v -> (match ist.goalopt with | None -> v - | Some g -> match_context_interp ist lr lmr g) + | Some g -> + match_context_interp ist lr lmr g) (* The closure system does not work yet. It must be better studied. *) (* (* Relaunch *) match_context_interp ist' lr lmr g)*) | v -> v |