aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
2011-09-26Adding subst_term up to convherbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-09-25Polishing commits r14492, r14448 and r14407 (tactics propagateherbelin
2011-09-25Not hard-wiring camlp5 path in target source-doc!herbelin
2011-09-24Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutherbelin
2011-09-24Completing r14448 and thus continuing r14407 (using Cast to propagateherbelin
2011-09-23Fix commit 14489: missing Coq. in dirpathletouzey
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
2011-09-23Program: add some check_required_library (fix #2592) + some dead code removalletouzey
2011-09-22Remove specific hash-consing of Term.types (was unused anyway)letouzey
2011-09-22Hash-consing: attempt to stop hash-consing separately constr in declare.mlletouzey
2011-09-22Remove duplicated version of check_required_library.letouzey
2011-09-22test-suite : an additional message displayed by Notation2.vletouzey
2011-09-22Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.letouzey
2011-09-22Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).herbelin
2011-09-19Makefile.doc: typo, index_url.txt should be index_urls.txtletouzey
2011-09-19Fix test-suite/ide for repository compiled without -local (fix #2600)letouzey
2011-09-18avoid dependency nightmare by creating coqdep_{lexer,common}.mliletouzey
2011-09-17doc/refman/Extraction.tex: no need to actually build euclid.mlletouzey
2011-09-17Euclid: make the proof transparent (example of extraction in stdlib)letouzey
2011-09-17Various fixes in the Makefilesletouzey
2011-09-16Omega: for non-arithmetical goals, try proving False from context (wish #2236)letouzey
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
2011-09-15coqc: Recognize option -force-load-proofs.letouzey
2011-09-15Names.make_mbid and co : convert from/to identifier (avoid some String.copy)letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-09-09correction du bug 2047jforest
2011-09-08More twicks on hash-consingletouzey
2011-09-07Fix the hconsing of universesletouzey
2011-09-06make world now builds fake_ide (to please coq-bench)letouzey
2011-09-06Improved ltac code for zify (fix #2575).letouzey
2011-09-06test-suite/ide: misc improvementletouzey
2011-09-06Avoid registering λ and Π as keywords just for some private Local Notationletouzey
2011-09-06ide/preferences.ml: apparently no `META in Gdk.Tags.modifierletouzey
2011-09-06Ocamlbuild : build of fake_ideletouzey
2011-09-05fake_ide: a short program to mimic an ide talking to coqtop -ideslaveletouzey
2011-09-05Coqide: new backtracking code, based on the Backtrack commandletouzey
2011-09-05Ide_intf: slight reorganisation of the IDE apiletouzey
2011-09-05Lib: remove strange code about backtracking to the current stateletouzey
2011-09-05Lib.node: merge OpenedModtype and OpenedModule, same for Closed...letouzey
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-09-05Util.error now creates UserError(_,msg) instead of UserError(str,str)letouzey
2011-09-05Extraction Implicit: fix the numbering of constructor argumentsletouzey
2011-09-04Having added a special Cast for remembering the use of conversionherbelin
2011-09-03Bug 3596: ocamlbuild: coq_makefile now requires Unixpboutill
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:18:03 +0000