aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fix compilation error due to commented code in previous commit by Hugo.Gravatar Matthieu Sozeau2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
* Remove confusing behavior of unify_with_subterm that could fail withGravatar Matthieu Sozeau2014-08-14
* Fix non-printing of coercions for primitive projections (fixes bug #3433).Gravatar Matthieu Sozeau2014-08-14
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* Fix bug introduced by earlier commit on first-order unification of primitiveGravatar Matthieu Sozeau2014-08-10
* Fix unification which was failing when unifying a primitive projection againstGravatar Matthieu Sozeau2014-08-09
* Allow pattern matching on the applied form of projections with primitiveGravatar Matthieu Sozeau2014-08-09
* Do early occur-check in unification to allow eta to fire (fixes bug #3477)Gravatar Matthieu Sozeau2014-08-09
* Using the asymmetric merging primitive in Evd.Gravatar Pierre-Marie Pédrot2014-08-09
* Cleaning up interface of ContextSet.Gravatar Pierre-Marie Pédrot2014-08-09
* Tentative performance fix for Evd.merge_uctx.Gravatar Pierre-Marie Pédrot2014-08-09
* Fix evarconv not applying eta when it used to. Fixes bug#3319.Gravatar Matthieu Sozeau2014-08-08
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Small code simplification.Gravatar Pierre-Marie Pédrot2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* - Fix handling of opaque polymorphic definitions which were turned transparent.Gravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* - Fix has_undefined_evars not using its or_sorts argument anymore.Gravatar Matthieu Sozeau2014-08-03
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Fix coercion code to disallow using cumulativity in the domain of products, w...Gravatar Matthieu Sozeau2014-07-17
* Add interface function to replace new_Type ()Gravatar Matthieu Sozeau2014-07-14
* Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Gravatar Matthieu Sozeau2014-07-10
* Revert patch making the oracle be used for the transparent state in evarconv,Gravatar Matthieu Sozeau2014-07-09
* In flex-flex cases, the undefinedness of an evar can not be preseved after co...Gravatar Matthieu Sozeau2014-07-07
* Missing check of evar instantiation, resulting in missing constraints (bug fr...Gravatar Matthieu Sozeau2014-07-07
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* Fix a Not_found anomaly raised by solve_evar_evar, we were breaking theGravatar Matthieu Sozeau2014-07-02
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Clarifying 'No such bound variable' message in apply, as suggested in #2387Gravatar Hugo Herbelin2014-06-30
* When building on-the-fly elimination principles, set the predicates universe ...Gravatar Matthieu Sozeau2014-06-29
* Really honor the [simpl never] flag in whd_simpl, it was still doing reductio...Gravatar Matthieu Sozeau2014-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:30:38 +0000