diff options
| author | Hugo Herbelin | 2015-07-31 21:31:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 15:06:53 +0200 |
| commit | 2418cf8d5ff6f479a5b43a87c861141bf9067507 (patch) | |
| tree | c9c9f026f3f5f2c2951a668bcf05f909ecfaa80c /tactics | |
| parent | cb0dea2a0c2993d4ca7747afc61fecdbb1c525b1 (diff) | |
Granting Jason's request for an ad hoc compatibility option on
considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).
Also updating and fixing wrong comments in test apply.v.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 402a9e88a1..6d81a48705 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -109,6 +109,24 @@ let _ = optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } +(* Compatibility option useful in developments using apply intensively + in ltac code *) + +let universal_lemma_under_conjunctions = ref false + +let accept_universal_lemma_under_conjunctions () = + !universal_lemma_under_conjunctions + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "trivial unification in tactics applying under conjunctions"; + optkey = ["Universal";"Lemma";"Under";"Conjunction"]; + optread = (fun () -> !universal_lemma_under_conjunctions) ; + optwrite = (fun b -> universal_lemma_under_conjunctions := b) } + + (*********************************************) (* Tactics *) (*********************************************) @@ -1332,7 +1350,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) && not (isEvar (fst (whd_betaiota_stack sigma t))) - && not (isRel t && destRel t > n-i) + && (accept_universal_lemma_under_conjunctions () || not (isRel t)) then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in |