aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Oups, typo in previous commitGravatar herbelin2011-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed what looks like a (very old) useless f.o. unification passGravatar herbelin2011-06-12
| | | | | | made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | 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
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
| | | | | | | | - 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
* Fixes in pruning, do not fail if pruning is impossible due to typing ↵Gravatar msozeau2011-06-10
| | | | | | constraints but postpone evar-evar problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
* More fixes in pruning/restriction of evars during unification.Gravatar msozeau2011-06-09
| | | | | | | | - 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
* Fixes in pruning in unification.Gravatar msozeau2011-06-08
| | | | | | | | | 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
* - Fix restrict_hyps to not allow filtering on a variable required to ↵Gravatar msozeau2011-06-07
| | | | | | | | | 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
* Applying Enrico Tassi's patch for giving priority to delta over eta inGravatar herbelin2011-05-24
| | | | | | | 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
* Failing instead of switching to the coercion mechanism when VMcastGravatar herbelin2011-05-15
| | | | | | 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
* A better procedure for checking presence of undefined evars.Gravatar aspiwack2011-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge, Cumul moved to CUMULGravatar msozeau2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
| | | | | | | | | 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
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
| | | | | | | | | | "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
* Fixing bug in printing let-in binders in fix/cofixGravatar herbelin2011-04-24
| | | | | | (backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow betaiota when checking unification of the types of metas (fixes ATBR ↵Gravatar msozeau2011-04-20
| | | | | | contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unification of types of metavariables and error message for sort ↵Gravatar msozeau2011-04-16
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
| | | | | | | - 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
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - 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
* - Improve unification (beta-reduction, and same heuristic as evarconv for ↵Gravatar msozeau2011-04-13
| | | | | | reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unify meta types with the right flags, add betaiotazeta reduction to ↵Gravatar msozeau2011-04-13
| | | | | | unification (potentially harmful) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proper typing of metavariables, type errors were completely ignored ↵Gravatar msozeau2011-04-13
| | | | | | 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
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
| | | | | | - 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
* Catch NotArity exception and transform it into an anomaly in retyping.Gravatar msozeau2011-04-11
| | | | | | | | | | 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
* Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vGravatar herbelin2011-04-08
| | | | | | 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
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
| | | | | | | 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
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
* As remarked by Enrico, we'd better use eq_constr than structural equalityGravatar herbelin2011-03-31
| | | | | | | (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
* - Remove useless grammar ruleGravatar msozeau2011-03-23
| | | | | | - 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
* - Fix solve_simpl_eqn which was cheking instances types in the wrong ↵Gravatar msozeau2011-03-23
| | | | | | | | 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
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
| | | | | | | | | | | | | | | | 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
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
| | | | | | | 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
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
| | | | | | | | | | | | | 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
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
| | | | | | | - 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
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
| | | | | | | in the 8.3 patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not forget conv_pbs when resetting an evm: Gravatar msozeau2011-03-10
| | | | | | | | | | - 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
* Solve evar instantiations in the right environment.Gravatar msozeau2011-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13899 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
| | | | | | | 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
* Revert commit r13883: instantiating ?n by a lambda when "?n a" has toGravatar herbelin2011-03-07
| | | | | | | | 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
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
| | | | | | | | 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
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
| | | | | | (in addition of types to names) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13887 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few more betaiota on environments and types of error messages. Seems toGravatar herbelin2011-03-05
| | | | | | be convenient in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for instantiation of ?n by a lambda when "?n a" has toGravatar herbelin2011-03-05
| | | | | | 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
* Reorganized a bit evarconv.ml:Gravatar herbelin2011-03-05
| | | | | | | | | | | | | | | - 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
* Improved define_evar_as_lambda which was creating an unrelated new evarGravatar herbelin2011-03-05
| | | | | | 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
* Instantiate evar by a lambda when "?n args" has to unify with ProdGravatar herbelin2011-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13880 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 06:44:52 +0000