diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 8 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 33 | ||||
| -rw-r--r-- | tactics/setoid_replace.mli | 2 |
3 files changed, 27 insertions, 16 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 480ca95609..ebba4b00bb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -556,12 +556,18 @@ let print_searchtable () = let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l) +(* tell auto not to reuse already instantiated metas in unification (for + compatibility, since otherwise, apply succeeds oftener) *) + +open Unification + +let auto_unif_flags = { modulo_delta = true; use_metas_eagerly = false } (* Try unification with the precompiled clause, then use registered Apply *) let unify_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver false clenv' gls in + let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in h_simplest_apply c gls (* builds a hint database from a constr signature *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 477beba4ab..fb25d9d25d 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -210,7 +210,9 @@ let coq_impl = lazy(constant ["Setoid_tac"] "impl") (************************* Table of declared relations **********************) -(* Relations are stored in a table which is synchronised with the Reset mechanism. *) +(* Relations are stored in a table which is synchronised with the + Reset mechanism. The table maps the term denoting the relation to + the data of type relation that characterises the relation *) let relation_table = ref Gmap.empty @@ -1464,12 +1466,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = (MApp (func,mor,a,output_direction))) output_directions @ res ) [] a' - | (he::tl) as a-> + | (he::tl) -> let typnf = Reduction.whd_betadeltaiota env typ in match kind_of_term typnf with - Cast (typ,_,_) -> - find_non_dependent_function env c c_args_rev typ - f_args_rev a_rev a | Prod (name,s,t) -> let env' = push_rel (name,None,s) env in let he = @@ -1564,12 +1563,12 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = match res' with [] when res = [] -> errorlabstrm "Setoid_rewrite" - (str "Either the term " ++ pr_lconstr t ++ str " that must be " ++ - str "rewritten occurs in a covariant position or the goal is not " ++ - str "made of morphism applications only. You can replace only " ++ - str "occurrences that are in a contravariant position and such that " ++ - str "the context obtained by abstracting them is made of morphism " ++ - str "applications only.") + (strbrk "Either the term " ++ pr_lconstr t ++ strbrk " that must be " ++ + strbrk "rewritten occurs in a covariant position or the goal is not" ++ + strbrk " made of morphism applications only. You can replace only " ++ + strbrk "occurrences that are in a contravariant position and such " ++ + strbrk "that the context obtained by abstracting them is made of " ++ + strbrk "morphism applications only.") | [] -> errorlabstrm "Setoid_rewrite" (str "No generated set of side conditions is a superset of those " ++ @@ -1732,18 +1731,22 @@ let check_evar_map_of_evars_defs evd = (* [unification_rewrite] searchs a match for [c1] in [but] and then returns the modified objects (in particular [c1] and [c2]) *) +let rewrite_unif_flags = { modulo_delta = false; use_metas_eagerly = true } +let rewrite2_unif_flags = { modulo_delta = true; use_metas_eagerly = true } + let unification_rewrite c1 c2 cl but gl = let (env',c1) = try - (* ~mod_delta:false to allow to mark occurences that must not be + (* ~flags:(false,true) to allow to mark occurences that must not be rewritten simply by replacing them with let-defined definitions in the context *) - w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.evd + w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd with Pretype_errors.PretypeError _ -> - (* ~mod_delta:true to make Ring work (since it really + (* ~flags:(true,true) to make Ring work (since it really exploits conversion) *) - w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.evd + w_unify_to_subterm ~flags:rewrite2_unif_flags + (pf_env gl) (c1,but) cl.evd in let cl' = {cl with evd = env' } in let c2 = Clenv.clenv_nf_meta cl' c2 in diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index ecad6a574e..2dd153b3ff 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -79,3 +79,5 @@ val new_named_morphism : val relation_table_find : constr -> relation val relation_table_mem : constr -> bool + +val prrelation : relation -> Pp.std_ppcmds |