aboutsummaryrefslogtreecommitdiff
path: root/pretyping/tacred.mli
AgeCommit message (Expand)Author
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-10-30Reduction functions based on CClosure should take an envMaxime Dénès
2018-09-10[dune] Add apidoc target using `odoc`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up interfaces.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-06-28Moved code for finding subterms (pattern, induction, set, generalize, ...)Hugo Herbelin
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-11-21Configurable simpl tacticgareuselesinge
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-10-28Remove old compatibility stuff (Tacred.nf)glondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2007-04-13Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantherbelin
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-02-07Amélioration des messages d'erreurs de tacred; unfold considère maintenant leherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:51 +0000