diff options
| author | Hugo Herbelin | 2014-11-27 22:30:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-27 23:37:31 +0100 |
| commit | a9fd21ac2b2e3908d8eb8d5a549c43949cddc69a (patch) | |
| tree | b6e897f501785ccc38df16df854479d0754a92c4 /tactics | |
| parent | 8ff32fd0748b0d1d7bd0a7612e05c26236b65d48 (diff) | |
Reverting the following block of three commits:
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index a7fc38a23a..d6083860a9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -170,9 +170,8 @@ let instantiate_lemma gl c ty l l2r concl = let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in [eqclause] -let rewrite_conv_closed_core_unif_flags env = - let ts = Conv_oracle.get_transp_state (Environ.oracle env) in { - modulo_conv_on_closed_terms = Some ts; +let rewrite_conv_closed_core_unif_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -198,18 +197,17 @@ let rewrite_conv_closed_core_unif_flags env = modulo_eta = true; } -let rewrite_conv_closed_unif_flags env = - let flags = rewrite_conv_closed_core_unif_flags env in { - core_unify_flags = flags; - merge_unify_flags = flags; - subterm_unify_flags = flags; +let rewrite_conv_closed_unif_flags = { + core_unify_flags = rewrite_conv_closed_core_unif_flags; + merge_unify_flags = rewrite_conv_closed_core_unif_flags; + subterm_unify_flags = rewrite_conv_closed_core_unif_flags; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = false } let rewrite_elim with_evars frzevars cls c e = Proofview.Goal.enter begin fun gl -> - let flags = make_flags frzevars (Proofview.Goal.sigma gl) (rewrite_conv_closed_unif_flags (Proofview.Goal.env gl)) c in + let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in general_elim_clause with_evars flags cls c e end |