diff options
| author | herbelin | 2010-06-06 14:04:29 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-06 14:04:29 +0000 |
| commit | c3d45696c271df086c39488d8a86fd2b60ec8132 (patch) | |
| tree | a22e546d4648697d31ec02e23d577d82a7f3fd7d /tactics/tauto.ml4 | |
| parent | 5cfed41826bb2c1cb6946bc53f56d93232c98011 (diff) | |
Added support for Ltac-matching terms with variables bound in the pattern
- Instances found by matching.ml now collect the set of bound
variables they possibly depend on in the pattern (see type
Pattern.extended_patvar_map); the variables names are canonically
ordered so that non-linear matching takes actual names into account.
- Removed typing of matching constr instances in advance (in
tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback
is that we may have to re-type several times the same term but it is
necessary for considering terms with locally bound variables of which
we do not keep the type (and if even we had kept the type, we would have
to adjust the indices to the actual context the term occurs).
- A bit of documentation of pattern.mli, matching.mli and pretyping.mli.
- Incidentally add env while printing idtac messages. It seems more correct
and I hope I did not break some intended existing behavior.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 2bb225c667..ef0d62285f 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -22,7 +22,7 @@ open Genarg let assoc_var s ist = match List.assoc (Names.id_of_string s) ist.lfun with - | VConstr c -> c + | VConstr ([],c) -> c | _ -> failwith "tauto: anomaly" (** Parametrization of tauto *) @@ -114,8 +114,8 @@ let flatten_contravariant_conj ist = | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then - let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in - let hyp = valueIn (VConstr hyp) in + let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in + let hyp = valueIn (VConstr ([],hyp)) in let intros = iter_tac (List.map (fun _ -> <:tactic< intro >>) args) <:tactic< idtac >> in @@ -149,9 +149,9 @@ let flatten_contravariant_disj ist = | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then - let hyp = valueIn (VConstr hyp) in + let hyp = valueIn (VConstr ([],hyp)) in iter_tac (list_map_i (fun i arg -> - let typ = valueIn (VConstr (mkArrow arg c)) in + let typ = valueIn (VConstr ([],mkArrow arg c)) in <:tactic< let typ := $typ in let hyp := $hyp in |