aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Expand)AuthorAge
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Fix non-printing of coercions for primitive projections (fixes bug #3433).Gravatar Matthieu Sozeau2014-08-14
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* Move to a representation of universe polymorphic constants using indices for ...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
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Quick fix of bug #2996 continued (case of inductive types).Gravatar Hugo Herbelin2014-06-28
* Deactivate the "Standard Propositions Naming" flag, source of a lot ofGravatar Hugo Herbelin2014-06-26
* Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...Gravatar Matthieu Sozeau2014-06-25
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Check a list length before doing a List.chop (fix #3000)Gravatar letouzey2013-03-20
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
* Noise for nothingGravatar pboutill2012-03-02
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 22:18:26 +0000