aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2011-06-12Removed what looks like a (very old) useless f.o. unification passherbelin
made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Moved allow_K to a unification flagherbelin
- seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing ↵msozeau
constraints but postpone evar-evar problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
- Do not allow to filter variables that appear in the conclusion of an evar. - Do not attempt to restrict evars based on a substitution that does not contain only evars (fall back to the pattern fragment and do not lose solutions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-08Fixes in pruning in unification.msozeau
Properly normalize evars to reflect the already pruned evars in the type of dependent evars to allow more precise restriction of hyps. Directly check the type of an evar instance, allowing backtracking on ill-typed instanciations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to ↵msozeau
typecheck the evar's conclusion - Prevent extend_evar from creating ill-formed evars with de Bruijn-open conclusions. - Minor fix of define_evars_as_lambda, another mixup of named and de Bruijn indices. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14163 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-24Applying Enrico Tassi's patch for giving priority to delta over eta inherbelin
unification (evarconv.ml). Works better for compiling math. comp. library while seems ok on other examples. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14153 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-15Failing instead of switching to the coercion mechanism when VMcastherbelin
involves evars (seem cleaner) at type-inference time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14123 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Fix merge, Cumul moved to CUMULmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14093 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
"apply" unification. Assuming w_unify_0 is not eventually abandoned, it remains to merge unify_with_eta into unify_0 (what unify_with_eta does and that unify_0 does not do is to select of two instances of the same meta the one with less lambda's; it is unclear whether this is useful heuristic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14091 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
(backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14055 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-20Allow betaiota when checking unification of the types of metas (fixes ATBR ↵msozeau
contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14032 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-18Add a flag to control betaiota reduction during unification to maintain ↵msozeau
backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-16Fix unification of types of metavariables and error message for sort ↵msozeau
unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Make typeclass transparency information directly availablemsozeau
- Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Remove create_evar_defsmsozeau
- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Improve unification (beta-reduction, and same heuristic as evarconv for ↵msozeau
reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Unify meta types with the right flags, add betaiotazeta reduction to ↵msozeau
unification (potentially harmful) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Proper typing of metavariables, type errors were completely ignored ↵msozeau
before... Use sort constraint checking as in evarconv as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13990 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
- Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-11Catch NotArity exception and transform it into an anomaly in retyping.msozeau
Add a temporary fix in solve_simple_eqn to catch anomalies coming from retyping because the unification algorithm with metas doesn't respect the precondition that evar instances should be well-typed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
which did not test what it was supposed to test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13970 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
when a "match" is kernel-ill-typed (probably rarely visible from end user anyway but useful for debugging) + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06A few extra combinators about rel_declaration/named_declaration + a bit of docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-31As remarked by Enrico, we'd better use eq_constr than structural equalityherbelin
(it is a priori optimized but also able to reason modulo equality of names and modulo alpha-conversion). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23- Remove useless grammar rulemsozeau
- Better printing of unif constraints in evar_map's git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13925 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong ↵msozeau
environment sometimes. - Remove compilation warning in classes.ml due to (as yet) unused code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13924 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
in preparation for adding forward reasoning to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11- Better error messages taking unif. constraints into account.msozeau
- Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-10Do not forget conv_pbs when resetting an evm: msozeau
- In clenv, this used to forget the existing constraints, there are none in the other evar_map. - Other uses (evar_refiner, class_tactics) always reset with an enriched version of the same evar_map. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13901 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-08Solve evar instantiations in the right environment.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13899 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
be unified with a (truly) rigid term would need to be able to project non-atomic arguments of evars what is not done (consider e.g. "Check (fun m n (H:m+n=n) => ((f_equal _ H) : S (m+n) = S n))."). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13894 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Added a table for using reserved names for binding names to typesherbelin
(in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05A few more betaiota on environments and types of error messages. Seems toherbelin
be convenient in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13884 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Added support for instantiation of ?n by a lambda when "?n a" has toherbelin
be unified with a (truly) rigid term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13883 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Reorganized a bit evarconv.ml:herbelin
- Made a distinction between truly rigid constructions (Rigid) and possibly flexible constructions (match/fix/meta, now called PseudoRigid) that are currently assimilated to rigid by lack of appropriate study of their flexibility. One day, the flexibility of these pseudo-rigid constructions will have to considered seriously. - Removed useless Cast/Cast cases in Rigid/Rigid block (Cast are removed in advance and LetIn are not considered Rigid). - Moved LetIn into the MaybeFlexible class. - Moved the Lambda/Lambda case upwards to factorize the rules for eta-expansion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13882 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
for the domain instead of retrieving the known domain of the initial evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13881 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Instantiate evar by a lambda when "?n args" has to unify with Prodherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13880 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-17- Use transparency information all the way through unification andmsozeau
conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
were all declared as global). - Add possibility to remove hints (Resolve or Immediate only) based on the name of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13842 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-23 21:21:12 +0000