aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-02Merge PR #8895: gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlPierre-Marie Pédrot
2018-11-02Merge PR #8809: [dev doc] Update proof engine docs, fixes #6640Pierre-Marie Pédrot
2018-11-02Expose Typing.judge_of_applyGaëtan Gilbert
This can be useful to avoid [Typing.type_of (App (f,args))] when working with universe polymorphism.
2018-11-02Remove ml4 from Coq's make build systemGaëtan Gilbert
2018-11-02Select OS specific coqide code with cp.Gaëtan Gilbert
2018-11-02Fix for coq/coq#8515 (command driven attributes)Gaëtan Gilbert
2018-11-02Add dev/changes about attribute syntax in mlgGaëtan Gilbert
2018-11-02Add overlays (command driven attributes)Gaëtan Gilbert
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
I think for instance the new code in this diff is cleaner and more systematic: ~~~diff VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater } -> { - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END ~~~
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Per command attribute parsing for core commandsGaëtan Gilbert
2018-11-02Add comment in stm to unsupport attributes for special commandsGaëtan Gilbert
2018-11-02Load doesn't support attributesGaëtan Gilbert
2018-11-02Simplify use of polymorphism/program globals in attributesGaëtan Gilbert
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-11-02Remove incorrect is_universe_polymorphism from modinternGaëtan Gilbert
2018-11-02rewrite: attributes handle is_univ_poly, is_program_modeGaëtan Gilbert
2018-11-02Remove is_universe_polymorphism in funindGaëtan Gilbert
Funind doesn't support polymorphism.
2018-11-02Remove is_universe_polymorphic in indschemesGaëtan Gilbert
2018-11-02Remove evdref style in build_combined_schemeGaëtan Gilbert
2018-11-02Generalize attributes further to get a monad (mostly for [map])Gaëtan Gilbert
Having [map] means we can structure attributes when combining them, eg get an attribute for [type universe_data = { poly : bool option; template : bool option }] from 2 [bool option] attributes. Using the previous representation we would have had to provide the inverse function [universe_data -> bool option * bool option] as well. An alternate way to get (++) is let (++) (x:'a t) (y:'b t) : ('a*'b) t = x >>= fun xv -> y >>= fun yv -> return (xv,yv) Not sure if that would be cleaner.
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes.
2018-11-02Remove pointless optional arguments to mk_attsGaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert
2018-11-02Remove location field from attributesGaëtan Gilbert
It was never set, because it makes no sense.
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
With camlp4 this file was not created but now that we use mlg it has appeared.
2018-11-02[dev doc] Update proof engine docs, fixes #6640Emilio Jesus Gallego Arias
We update the docs for the removal of `Sigma` and the deprecation of `enter_nf`.
2018-11-02Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).Hugo Herbelin
2018-11-01Fix alphabetical orderVincent Semeria
2018-11-01develop constructive epsilonVincent Semeria
2018-11-01Fix creditsVincent Semeria
2018-11-01Fix header and doc indexVincent Semeria
2018-11-01proof that R is uncountableVincent Semeria
2018-11-01Merge PR #8845: Fix typos in the document about CICThéo Zimmermann
2018-10-31Fixes rest of #3468 (tactic-in-term was not respecting scopes).Hugo Herbelin
We do it by passing interning env to ltac interning. Collecting scopes was already done by side-effect internally to Constrintern. We expose the side-effect to ltac.
2018-10-31Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).Hugo Herbelin
We compute the binding to tactic-in-term once for all in the right scopes before interpreting the tactic. An alternative would have been to surround the constr_expr by CDelimiters to simulate its interpretation in the expected scopes (though this would not have worked for temporary scopes).
2018-10-31Clarify meaning of boolean in IPatDispatchMaxime Dénès
2018-10-31[ssr] better doc for the IPatDispatch ASTEnrico Tassi
2018-10-31test-suite entry for issue #8544Cyril Cohen
2018-10-31[ssr] use tclDISPATCH for IPatDispatch (fix #8544)Enrico Tassi
2018-10-31Use standard combinator for Global.set_strategyMaxime Dénès
2018-10-31Introduce Safe_typing.set_share_reductionMaxime Dénès
2018-10-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
This emphasizes that it works only on inductive types. Also, the name is_template_polymorphic will be reused for a more general version.
2018-10-31Merge PR #8752: Enable fragile pattern warning in cclosureMaxime Dénès
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception ↵Hugo Herbelin
Ltac_plugin.Taccoerce.CannotCoerceTo.
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
See also 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b
2018-10-31Merge PR #8841: Share the construction of the evar instance in ↵Matthieu Sozeau
Clenv.make_evar_clause.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 16:37:37 +0000