aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-08-30Porting Hendrik's 8.3 patch for proof tree visualization under proofherbelin
2011-08-18Remove old file (1999)msozeau
2011-08-12Fixes mini-bug: Qed would succeed even on focused proofs.aspiwack
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-10Fixing typos in commentsherbelin
2011-08-10Graceful error message for [Proof Mode] and [Set Default Proof Mode] when req...aspiwack
2011-07-11Stores bullet stack on locally at the level of focuses rather than globally i...aspiwack
2011-07-06Fixed bullets so that they would play well with { }.aspiwack
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-07Catch AbstractionOverMeta as a unification failure in precatchable_exception.msozeau
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-17Fixes bug in [maximal_unfocus] introduced in r14120.aspiwack
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
2011-05-13The modules in proofs now use the Errors module to explain their exceptions t...aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-04-29Fixed a bug causing inconsistent states during proof editting.aspiwack
2011-04-29Some comments.aspiwack
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-02-22Try to fix the behavior of clenv_missing used when declaring hintsletouzey
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-02-10Started to fix the declarative proof mode (C-zar).aspiwack
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 04:24:03 +0000