aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
Commit message (Expand)AuthorAge
...
* More monomorphizationsGravatar ppedrot2012-11-13
* Updating headers.Gravatar herbelin2012-08-08
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Remove specific hash-consing of Term.types (was unused anyway)Gravatar letouzey2011-09-22
* More twicks on hash-consingGravatar letouzey2011-09-08
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Extraction: replace generic = on mutual_inductive_body by mib_equalGravatar puech2011-07-29
* Term: moved function constr_ord (a.k.a compare_constr) from Sequent to TermGravatar puech2011-07-29
* Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...Gravatar puech2011-07-29
* Term: added function eq_named_declarationGravatar puech2011-07-29
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
* Reintroduce kind_of_type (used by Presburger contrib)Gravatar glondu2010-10-05
* Remove kind_of_type, kind_of_term2 (dead code)Gravatar glondu2010-09-28
* Partial review of removed dead code (r13460)Gravatar herbelin2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* "make source-doc" builds documentation of mli in html and pdf atGravatar pboutill2010-04-29
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Minor unification changes:Gravatar msozeau2009-05-18
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Fix a few bugs in Program: use user-given typing constraints forGravatar msozeau2008-03-09
* Finish let| implementation and document itGravatar msozeau2008-01-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Suite restructuration unification et division des problèmesGravatar herbelin2007-05-23
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Ajout fold_rel_declaration et fold_named_declarationGravatar herbelin2006-10-27
* Export de closedn pour EvarutilGravatar herbelin2006-08-28
* Ajout substl_named_decl pour mode MapleGravatar herbelin2006-05-23
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23