aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-22micromega: remove empty file CheckerMakerletouzey
2013-08-22Field_theory : faster and nicer proofs + nice notations.letouzey
2013-08-22Ring_polynom : shorter proof for Psub_okletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-08calling interp by hand is forbiddengareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
2013-08-03Replacing an association list by a map in globalizing environment.ppedrot
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
2013-07-17Lib.contents () instead of Lib.contents_after Noneletouzey
2013-07-17Extraction : message about lack of support for toplevel Includeletouzey
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
2013-06-25Useless use of maps in constr internalizing.ppedrot
2013-06-22Now, idtac closures use maps instead of association list.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-21Revert "parse "of" as KEYID "of""gareuselesinge
2013-06-19parse "of" as KEYID "of"gareuselesinge
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
2013-06-10Hiding tactic value representations.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-05-30bwaa, a Pervasive.comparepboutill
2013-05-29newring.ml4: interp constr arg at interp time (not parse time)gareuselesinge
2013-05-12Removing Gmap from Extraction pluginppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-05-05Little fix for Nsatz: hypotheses not directly relevant to the nsatzherbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-23Indfun : use States.with_state_protection instead of freeze/unfreezeletouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-04-11Backport r16394 from 8.4:msozeau
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-18Extraction AccessOpaque is now activated again by default (#2952)letouzey
2013-03-15Extract_env : correct exceptions mentionned in a try ... withletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 08:52:21 +0000