aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-06-12Changing the type of Ltac values. Now they are toplevel genericppedrot
2013-06-12Fixing a Not_found and evar not found anomaly found in ATBR,msozeau
2013-06-12One more fix for rewrite: disallow resolving of the (partial) constraintsmsozeau
2013-06-10Hiding tactic value representations.ppedrot
2013-06-10Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...msozeau
2013-06-07Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd msozeau
2013-06-06Fixing bug #3030.ppedrot
2013-06-06Fixing #3056ppedrot
2013-06-06More comments in Genarg.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-06-06Document changes and add missing documentation for Program options.msozeau
2013-06-06Add an option to shrink the context of program obligations to avoidmsozeau
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-06-05Use a Summary.ref for the tactic in tactic options for proper backtrackingmsozeau
2013-06-04Backtrack on unneeded change of interface for pose_metas_as_evars.msozeau
2013-06-04Start documenting new [rewrite_strat] tactic that applies rewritingmsozeau
2013-06-02A constructive proof of Fan theorem where paths are represented by predicates.herbelin
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-06-02Flags V8_4 for compatibility infrastructure.herbelin
2013-06-02Fixing a typo in the documentation of discriminate.herbelin
2013-06-02Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anherbelin
2013-06-02Fixing buggy backtracking in "intros * pat" with failing "pat".herbelin
2013-06-02Modest protection against "injection" and co raising anomaly inherbelin
2013-05-30Removing a useless location in ltac trace mechanism.ppedrot
2013-05-30Do not compute fallback eagerly in Evarconvpboutill
2013-05-30export Unification.abstract_list_all_with_dependenciespboutill
2013-05-30Why not going inside fixpoint definition with appcontext ?pboutill
2013-05-30comments in mlipboutill
2013-05-30bwaa, a Pervasive.comparepboutill
2013-05-29newring.ml4: interp constr arg at interp time (not parse time)gareuselesinge
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
2013-05-29Documenting the "appcontext" by default.ppedrot
2013-05-29More clever implemenation for IStream.ppedrot
2013-05-28Setting "appcontext" as the default behaviour in Ltac matching.ppedrot
2013-05-28Fixing warning of deprecated Argument Scopes.ppedrot
2013-05-28Getting rid of LtacLocated exception transformer.ppedrot
2013-05-28Fixing debug of empty Ltac matching goal.ppedrot
2013-05-28Pushing lazy lists into Ltac. Now, the control flow is explicitppedrot
2013-05-28Adding a persistent stream data structure.ppedrot
2013-05-24Code cleaning in Matching.ppedrot
2013-05-23Fixing #3042ppedrot
2013-05-16Fixing Pp.strbrk which was reversing words.ppedrot
2013-05-16std_ppcmds is persistent, errors can be printed twicegareuselesinge
2013-05-14Mini documentation (evar_absorb_arguments).herbelin
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-05-14"change ... in ..." and "simpl ... in ..." now consider nestedherbelin
2013-05-14Fixing a regression in unification introduced in r16205 (error raisedherbelin
2013-05-14Gmap is now useless, hail to Map!ppedrot
2013-05-14Removing the use of Gmap from Auto.ppedrot
2013-05-14Removing Gmap from Classops. Fold order only mattered for printing.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 08:45:51 +0000