aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
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
2011-02-11An automatic substitution of scope at functor applicationletouzey
For Argument Scope, we now record types (more precisely classes cl_typ) in addition to scope list. After substitution (e.g. at functor application), the new types are used to search for corresponding concrete scopes. Currently, this automatic scope substitution of argument scope takes precedence (if successful) over scope declared in the functor (even by the user). On the opposite, the manual scope substitution (cf last commit introducing annotation [scope foo to bar]) is done _after_ the automatic scope substitution. TODO: if this behavior is satisfactory, document it ... Note that Classops.find_class_type lose its env args since it was actually unused, and is now used for Notation.find_class git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13840 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13833 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-03Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)letouzey
After r13717, we concentrate on undefined evars. But doing so too naively was breaking Class_tactics.split_evars, since defined evars may point to undefined ones. We should not ignore them, but rather traverse them, which is now done by functions Evarutil.undefined_evars_of_* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13809 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-27Make simpl use the proper constant when folding (mutual) fixpointsletouzey
Before this commit, when simpl was finding the constant name for folding some (mutual) fixpoint, this was done via some repr_con followed by make_con. Problem: this doesn't preserve the canonical part of a Names.constant. For instance the following script was buggish: Module M. Fixpoint foo n := match n with O => O | S n => bar n end with bar n := match n with O => O | S n => foo n end. End M. Module N. Include M. (* foo, bar have here "user name" N but "canonical name" M *) Eval simpl in (fun x => bar (S x)). (* Anomaly: uncaught exception Failure "Cannot print a global reference". *) (* since simpl has produce a different bar with both user and canonical N *) TODO : check all other uses of make_con in the rest of the sources... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13803 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11ratrapage exception, deja fait ...bgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13782 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13781 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07mli comments for docpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13773 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
perl -pi -e 's/(mk)R(Ref|Var|Evar|PatVar|App|Lambda|Prod|LetIn|Case s|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic|Prop|Type|Fix|CoFix|Struct Rec|WfRec|MeasureRec)/\1G\2/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13758 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24More {raw => glob} changes for consistencyglondu
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-23Rename rawterm.ml into glob_term.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 06:52:33 +0000