aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml15
-rw-r--r--COMPATIBILITY7
-rw-r--r--dev/build/windows/makecoq_mingw.sh2
-rw-r--r--doc/refman/RefMan-tac.tex39
-rw-r--r--engine/uState.ml125
-rw-r--r--ide/coqidetop.mllib1
-rw-r--r--ide/ide_slave.ml10
-rw-r--r--ide/texmacspp.ml766
-rw-r--r--ide/texmacspp.mli12
-rw-r--r--kernel/uGraph.mli1
-rw-r--r--plugins/.dir-locals.el4
-rw-r--r--tactics/equality.ml19
-rw-r--r--tactics/equality.mli3
-rw-r--r--tactics/tactics.ml40
-rw-r--r--test-suite/Makefile5
-rw-r--r--test-suite/output/Tactics.out4
-rw-r--r--test-suite/output/Tactics.v10
-rw-r--r--toplevel/coqtop.ml3
-rw-r--r--toplevel/vernac.ml23
-rw-r--r--vernac/obligations.ml12
20 files changed, 208 insertions, 893 deletions
diff --git a/.travis.yml b/.travis.yml
index aa2e0e63c8..a959fbf961 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,14 +1,21 @@
dist: trusty
+
# Travis builds are slower using sudo: false (the container-based
# infrastructure) as of March 2017; see
# https://github.com/coq/coq/pull/467 for some discussion.
sudo: required
+
# Until Ocaml becomes a language, we set a known one.
language: c
+
cache:
apt: true
directories:
- $HOME/.opam
+
+before_cache:
+ - rm -rf ~/.opam/log/
+
addons:
apt:
sources:
@@ -17,6 +24,7 @@ addons:
- opam
- aspcud
- gcc-multilib
+
env:
global:
- NJOBS=2
@@ -55,9 +63,8 @@ matrix:
allow_failures:
- env: TEST_TARGET="ci-geocoq"
- # Full Coq test-suite with two compilers
- # [TODO: use yaml refs and avoid duplication for packages list]
include:
+ # Full Coq test-suite with two compilers
- env:
- TEST_TARGET="test-suite"
- EXTRA_CONF="-coqide opt -with-doc yes"
@@ -81,6 +88,7 @@ matrix:
- ghostscript
- transfig
- imagemagick
+
- env:
- TEST_TARGET="test-suite"
- COMPILER="4.04.1"
@@ -92,6 +100,8 @@ matrix:
sources:
- avsm
packages: *extra-packages
+
+ # Ocaml warnings with two compilers
- env:
- TEST_TARGET="coqocaml"
- EXTRA_CONF="-coqide opt -warn-error"
@@ -107,6 +117,7 @@ matrix:
- aspcud
- libgtk2.0-dev
- libgtksourceview2.0-dev
+
- env:
- TEST_TARGET="coqocaml"
- COMPILER="4.04.1"
diff --git a/COMPATIBILITY b/COMPATIBILITY
index d423e71df3..78dfabaa3e 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,10 @@
+Potential sources of incompatibilities between Coq V8.6 and V8.7
+----------------------------------------------------------------
+
+- Extra superfluous names in introduction patterns may now raise an
+ error rather than a warning when the superfluous name is already in
+ use. The easy fix is to remove the superfluous name.
+
Potential sources of incompatibilities between Coq V8.5 and V8.6
----------------------------------------------------------------
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 52b158871b..98e80c7652 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1082,7 +1082,7 @@ function make_coq {
copq_coq_gtk
copy_coq_license
- # make clean seems to br broken for 8.5pl2
+ # make clean seems to be broken for 8.5pl2
# 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
# 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
# make clean
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 87b9e4914f..fc3fdd0025 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2187,32 +2187,24 @@ the given bindings to instantiate parameters or hypotheses of {\term}.
\label{injection}
\tacindex{injection}
-The {\tt injection} tactic is based on the fact that constructors of
-inductive sets are injections. That means that if $c$ is a constructor
-of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
-terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
-too.
+The {\tt injection} tactic exploits the property that constructors of
+inductive types are injective, i.e. that if $c$ is a constructor
+of an inductive type and $c~\vec{t_1}$ and $c~\vec{t_2}$ are equal
+then $\vec{t_1}$ and $\vec{t_2}$ are equal too.
If {\term} is a proof of a statement of conclusion
{\tt {\term$_1$} = {\term$_2$}},
-then {\tt injection} applies injectivity as deep as possible to
-derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
-placed in the same positions. For example, from {\tt (S
- (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}. To use this
-tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
-set and they should be neither explicitly equal, nor structurally
-different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
-their respective normal forms, then:
-\begin{itemize}
-\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
-\item there must not exist any pair of subterms {\tt u} and {\tt w},
- {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
- placed in the same positions and having different constructors as
- head symbols.
-\end{itemize}
-If these conditions are satisfied, then, the tactic derives the
-equality of all the subterms of {\term$_1$} and {\term$_2$} placed in
-the same positions and puts them as antecedents of the current goal.
+then {\tt injection} applies the injectivity of constructors as deep as possible to
+derive the equality of all the subterms of {\term$_1$} and {\term$_2$} at positions
+where {\term$_1$} and {\term$_2$} start to differ.
+For example, from {\tt (S p, S n) = (q, S (S m)} we may derive {\tt S
+ p = q} and {\tt n = S m}. For this tactic to work, {\term$_1$} and
+{\term$_2$} should be typed with an inductive
+type and they should be neither convertible, nor having a different
+head constructor. If these conditions are satisfied, the tactic
+derives the equality of all the subterms of {\term$_1$} and
+{\term$_2$} at positions where they differ and adds them as
+antecedents to the conclusion of the current goal.
\Example Consider the following goal:
@@ -2251,6 +2243,7 @@ context using \texttt{intros until \ident}.
\item \errindex{Not a projectable equality but a discriminable one}
\item \errindex{Nothing to do, it is an equality between convertible terms}
\item \errindex{Not a primitive equality}
+\item \errindex{Nothing to inject}
\end{ErrMsgs}
\begin{Variants}
diff --git a/engine/uState.ml b/engine/uState.ml
index c66af02bb9..e27d0536d6 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -131,84 +131,87 @@ let instantiate_variable l b v =
exception UniversesDiffer
let process_universe_constraints ctx cstrs =
+ let open Univ in
let univs = ctx.uctx_universes in
let vars = ref ctx.uctx_univ_variables in
let normalize = Universes.normalize_universe_opt_subst vars in
- let rec unify_universes fo l d r local =
+ let is_local l = Univ.LMap.mem l !vars in
+ let varinfo x =
+ match Univ.Universe.level x with
+ | None -> Inl x
+ | Some l -> Inr l
+ in
+ let equalize_variables fo l l' r r' local =
+ (** Assumes l = [l',0] and r = [r',0] *)
+ let () =
+ if is_local l' then
+ instantiate_variable l' r vars
+ else if is_local r' then
+ instantiate_variable r' l vars
+ else if not (UGraph.check_eq_level univs l' r') then
+ (* Two rigid/global levels, none of them being local,
+ one of them being Prop/Set, disallow *)
+ if Univ.Level.is_small l' || Univ.Level.is_small r' then
+ raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ else if fo then
+ raise UniversesDiffer
+ in
+ Univ.enforce_eq_level l' r' local
+ in
+ let equalize_universes l r local = match varinfo l, varinfo r with
+ | Inr l', Inr r' -> equalize_variables false l l' r r' local
+ | Inr l, Inl r | Inl r, Inr l ->
+ let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in
+ let inst = Univ.univ_level_rem l r r in
+ if alg then (instantiate_variable l inst vars; local)
+ else
+ let lu = Univ.Universe.make l in
+ if Univ.univ_level_mem l r then
+ Univ.enforce_leq inst lu local
+ else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+ | Inl _, Inl _ (* both are algebraic *) ->
+ if UGraph.check_eq univs l r then local
+ else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ in
+ let unify_universes (l, d, r) local =
let l = normalize l and r = normalize r in
if Univ.Universe.equal l r then local
else
- let varinfo x =
- match Univ.Universe.level x with
- | None -> Inl x
- | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic)
- in
- if d == Universes.ULe then
+ match d with
+ | Universes.ULe ->
if UGraph.check_leq univs l r then
(** Keep Prop/Set <= var around if var might be instantiated by prop or set
later. *)
- if Univ.Universe.is_level l then
- match Univ.Universe.level r with
- | Some r ->
- Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
- | _ -> local
- else local
+ match Univ.Universe.level l, Univ.Universe.level r with
+ | Some l, Some r ->
+ Univ.Constraint.add (l, Univ.Le, r) local
+ | _ -> local
else
- match Univ.Universe.level r with
+ begin match Univ.Universe.level r with
| None -> error ("Algebraic universe on the right")
- | Some rl ->
- if Univ.Level.is_small rl then
+ | Some r' ->
+ if Univ.Level.is_small r' then
let levels = Univ.Universe.levels l in
- Univ.LSet.fold (fun l local ->
- if Univ.Level.is_small l || Univ.LMap.mem l !vars then
- unify_universes fo (Univ.Universe.make l) Universes.UEq r local
- else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
- levels local
+ let fold l' local =
+ let l = Univ.Universe.make l' in
+ if Univ.Level.is_small l' || is_local l' then
+ equalize_variables false l l' r r' local
+ else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None))
+ in
+ Univ.LSet.fold fold levels local
else
Univ.enforce_leq l r local
- else if d == Universes.ULub then
- match varinfo l, varinfo r with
- | (Inr (l, true, _), Inr (r, _, _))
- | (Inr (r, _, _), Inr (l, true, _)) ->
- instantiate_variable l (Univ.Universe.make r) vars;
- Univ.enforce_eq_level l r local
- | Inr (_, _, _), Inr (_, _, _) ->
- unify_universes true l Universes.UEq r local
+ end
+ | Universes.ULub ->
+ begin match Universe.level l, Universe.level r with
+ | Some l', Some r' ->
+ equalize_variables true l l' r r' local
| _, _ -> assert false
- else (* d = Universes.UEq *)
- match varinfo l, varinfo r with
- | Inr (l', lloc, _), Inr (r', rloc, _) ->
- let () =
- if lloc then
- instantiate_variable l' r vars
- else if rloc then
- instantiate_variable r' l vars
- else if not (UGraph.check_eq univs l r) then
- (* Two rigid/global levels, none of them being local,
- one of them being Prop/Set, disallow *)
- if Univ.Level.is_small l' || Univ.Level.is_small r' then
- raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
- else
- if fo then
- raise UniversesDiffer
- in
- Univ.enforce_eq_level l' r' local
- | Inr (l, loc, alg), Inl r
- | Inl r, Inr (l, loc, alg) ->
- let inst = Univ.univ_level_rem l r r in
- if alg then (instantiate_variable l inst vars; local)
- else
- let lu = Univ.Universe.make l in
- if Univ.univ_level_mem l r then
- Univ.enforce_leq inst lu local
- else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
- | _, _ (* One of the two is algebraic or global *) ->
- if UGraph.check_eq univs l r then local
- else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ end
+ | Universes.UEq -> equalize_universes l r local
in
let local =
- Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
- cstrs Univ.Constraint.empty
+ Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty
in
!vars, local
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index 043ad6008b..df988d8f11 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -4,6 +4,5 @@ Xml_printer
Serialize
Richpp
Xmlprotocol
-Texmacspp
Document
Ide_slave
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 56ada9d132..dbca959eae 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -388,14 +388,8 @@ let interp ((_raw, verbose), s) =
let quit = ref false
-(** Serializes the output of Stm.get_ast *)
-let print_ast id =
- match Stm.get_ast id with
- | Some (expr, loc) -> begin
- try Texmacspp.tmpp expr loc
- with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
- end
- | None -> Xml_datatype.PCData "ERROR"
+(** Disabled *)
+let print_ast id = Xml_datatype.PCData "ERROR"
(** Grouping all call handlers together + error handling *)
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
deleted file mode 100644
index 05f1820cf2..0000000000
--- a/ide/texmacspp.ml
+++ /dev/null
@@ -1,766 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-open Constrexpr_ops
-
-let unlock loc =
- let start, stop = Loc.unloc loc in
- (string_of_int start, string_of_int stop)
-
-let xmlWithLoc loc ename attr xml =
- let start, stop = unlock loc in
- Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
-
-let get_fst_attr_in_xml_list attr xml_list =
- let attrs_list =
- List.map (function
- | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
- | _ -> [])
- xml_list in
- match List.flatten attrs_list with
- | [] -> (attr, "")
- | l -> (List.hd l)
-
-let backstep_loc xmllist =
- let start_att = get_fst_attr_in_xml_list "begin" xmllist in
- let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in
- [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
- let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
- let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
- match att1, att2 with
- | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
- | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
- | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
- | _ -> 0
-
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
-
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
-
-let xmlThm typ name loc xml =
- xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef typ name loc xml =
- xmlWithLoc loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation attr name loc xml =
- xmlWithLoc loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation attr name loc =
- xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst name ?(attr=[]) loc =
- xmlWithLoc loc "constant" (("name", name) :: attr) []
-
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
- xmlWithLoc loc "operator"
- (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
-
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
-
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
-
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
-
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
-
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
-
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
-
-let xmlReference ref =
- let name = Libnames.string_of_reference ref in
- let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
- let b, e = string_of_int i, string_of_int j in
- Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
-
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
-
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
-
-let xmlScope loc action ?(attr=[]) name xml =
- xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
-
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-
-let xmlSectionSubsetDescr name ssd =
- Element("sectionsubsetdescr",["name",name],
- [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule loc s =
- xmlWithLoc loc "declarexmlmodule" []
- (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
-
-let xmlTODO loc x =
- xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
- match n with
- | Anonymous -> "_"
- | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
- match s with
- | GProp -> "Prop"
- | GSet -> "Set"
- | GType _ -> "Type"
-
-let string_of_cast_sort c =
- match c with
- | CastConv _ -> "CastConv"
- | CastVM _ -> "CastVM"
- | CastNative _ -> "CastNative"
- | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
- match s with
- | LetStyle -> "Let"
- | IfStyle -> "If"
- | LetPatternStyle -> "LetPattern"
- | MatchStyle -> "Match"
- | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
- | SetItemLevel (sl, NumLevel n) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
- | SetItemLevel (sl, NextLevel) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
- | SetLevel i -> ["level", string_of_int i]
- | SetAssoc a ->
- begin match a with
- | NonA -> ["",""]
- | RightA -> ["associativity", "right"]
- | LeftA -> ["associativity", "left"]
- end
- | SetEntryType (s, _) -> ["entrytype", s]
- | SetOnlyPrinting -> ["onlyprinting", ""]
- | SetOnlyParsing -> ["onlyparsing", ""]
- | SetCompatVersion v -> ["compat", Flags.pr_version v]
- | SetFormat (system, (loc, s)) ->
- let start, stop = unlock loc in
- ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
- match l, a, many with
- | (Discharge, Logical, true) -> "Hypotheses"
- | (Discharge, Logical, false) -> "Hypothesis"
- | (Discharge, Definitional, true) -> "Variables"
- | (Discharge, Definitional, false) -> "Variable"
- | (Global, Logical, true) -> "Axioms"
- | (Global, Logical, false) -> "Axiom"
- | (Global, Definitional, true) -> "Parameters"
- | (Global, Definitional, false) -> "Parameter"
- | (Local, Logical, true) -> "Local Axioms"
- | (Local, Logical, false) -> "Local Axiom"
- | (Local, Definitional, true) -> "Local Parameters"
- | (Local, Definitional, false) -> "Local Parameter"
- | (Global, Conjectural, _) -> "Conjecture"
- | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
- let tlist =
- List.flatten
- (List.map
- (fun (loc_names, _, e) ->
- let names =
- (List.map
- (fun (loc, name) ->
- xmlCst (string_of_name name) loc) loc_names) in
- match e with
- | CHole _ -> names
- | _ -> names @ [pp_expr e])
- bl) in
- match tlist with
- | [e] -> e
- | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
- Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
- match lb with
- | CLocalDef ((loc, nam), ce, ty) ->
- let attrs = ["name", string_of_name nam] in
- let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in
- pp_expr ~attr:attrs value
- | CLocalAssum (namll, _, ce) ->
- let ppl =
- List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
- xmlTyped (ppl @ [pp_expr ce])
- | CLocalPattern _ ->
- assert false
-and pp_local_decl_expr lde = (* don't know what it is for now *)
- match lde with
- | AssumExpr (_, ce) -> pp_expr ce
- | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
- (* inductive_expr *)
- let b,e = Loc.unloc l in
- let location = ["begin", string_of_int b; "end", string_of_int e] in
- [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
- begin match cl_or_rdexpr with
- | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
- | RecordDecl (_, ldewwwl) ->
- List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
- end @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end @
- (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
- let attrs =
- match optid with
- | None -> []
- | Some (loc, id) ->
- let start, stop = unlock loc in
- ["begin", start; "end", stop ; "name", Id.to_string id] in
- let kind, expr =
- match roe with
- | CStructRec -> "struct", []
- | CWfRec e -> "rec", [pp_expr e]
- | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
- | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
- Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
- (* fixpoint_expr *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* fixpoint name *)
- [pp_recursion_order_expr optid roe] @
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
- (* Nota: it is like fixpoint_expr without (optid, roe)
- * so could be merged if there is no more differences *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* cofixpoint name *)
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
- match cpe with
- | CPatAlias (loc, cpe, id) ->
- xmlApply loc
- (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCstr (loc, ref, None, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], []);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatCstr (loc, ref, Some cpel1, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatAtom (loc, optr) ->
- let attrs = match optr with
- | None -> []
- | Some r -> ["name", Libnames.string_of_reference r] in
- xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
- | CPatOr (loc, cpel) ->
- xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
- | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
- xmlApply loc
- (xmlOperator "notation" loc ::
- [xmlOperator n loc;
- Element ("subst", [],
- [Element ("subterms", [],
- List.map pp_cases_pattern_expr subst_constr);
- Element ("recsubterms", [],
- List.map
- (fun (cpel) ->
- Element ("recsubterm", [],
- List.map pp_cases_pattern_expr cpel))
- subst_rec)]);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
- | CPatPrim (loc, tok) -> pp_token loc tok
- | CPatRecord (loc, rcl) ->
- xmlApply loc
- (xmlOperator "record" loc ::
- List.map (fun (r, cpe) ->
- Element ("field",
- ["reference", Libnames.string_of_reference r],
- [pp_cases_pattern_expr cpe]))
- rcl)
- | CPatDelimiters (loc, delim, cpe) ->
- xmlApply loc
- (xmlOperator "delimiter" ~attr:["name", delim] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCast _ -> assert false
-and pp_case_expr (e, name, pat) =
- match name, pat with
- | None, None -> xmlScrutinee [pp_expr e]
- | Some (loc, name), None ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop] [pp_expr e]
- | Some (loc, name), Some p ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop]
- [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
- | None, Some p ->
- xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
- xmlWith
- (List.map
- (fun (_, cpel, e) ->
- let ppcepl =
- List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
- let ppe = [pp_expr e] in
- xmlCase (ppcepl @ ppe))
- bel)
-and pp_token loc tok =
- let tokstr =
- match tok with
- | String s -> PCData s
- | Numeral n -> PCData (to_string n) in
- xmlToken loc [tokstr]
-and pp_local_binder_list lbl =
- let l = (List.map pp_local_binder lbl) in
- Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
- let l = List.map pp_expr cel in
- Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
- match e with
- | CRef (r, _) ->
- xmlCst ~attr
- (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
- | CProdN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CApp (loc, (_, hd), args) ->
- xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
- | CAppExpl (loc, (_, r, _), args) ->
- xmlApply ~attr loc
- (xmlCst (Libnames.string_of_reference r)
- (Libnames.loc_of_reference r) :: List.map pp_expr args)
- | CNotation (loc, notation, ([],[],[])) ->
- xmlOperator notation loc
- | CNotation (loc, notation, (args, cell, lbll)) ->
- let fmts = Notation.find_notation_extra_printing_rules notation in
- let oper = xmlOperator notation loc ~pprules:fmts in
- let cels = List.map pp_const_expr_list cell in
- let lbls = List.map pp_local_binder_list lbll in
- let args = List.map pp_expr args in
- xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
- | CSort(loc, s) ->
- xmlOperator (string_of_glob_sort s) loc
- | CDelimiters (loc, scope, ce) ->
- xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
- [pp_expr ce])
- | CPrim (loc, tok) -> pp_token loc tok
- | CGeneralization (loc, kind, _, e) ->
- let kind= match kind with
- | Explicit -> "explicit"
- | Implicit -> "implicit" in
- xmlApply loc
- (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
- | CCast (loc, e, tc) ->
- begin match tc with
- | CastConv t | CastVM t |CastNative t ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
- [pp_expr e; pp_expr t])
- | CastCoerce ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
- [pp_expr e])
- end
- | CEvar (loc, ek, cel) ->
- let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
- xmlApply loc
- (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
- ppcel)
- | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
- | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
- | CIf (loc, test, (_, ret), th, el) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "if" loc ::
- return @ [pp_expr th] @ [pp_expr el])
- | CLetTuple (loc, names, (_, ret), value, body) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "lettuple" loc ::
- return @
- (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
- [pp_expr value; pp_expr body])
- | CCases (loc, sty, ret, cel, bel) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
- (return @
- [Element ("scrutinees", [], List.map pp_case_expr cel)] @
- [pp_branch_expr_list bel]))
- | CRecord (_, _) -> assert false
- | CLetIn (loc, (varloc, var), value, typ, body) ->
- let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in
- xmlApply loc
- (xmlOperator "let" loc ::
- [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
- | CLambdaN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CCoFix (_, _, _) -> assert false
- | CFix (loc, lid, fel) ->
- xmlApply loc
- (xmlOperator "fix" loc ::
- List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
- fel))
-
-let pp_comment (c) =
- match c with
- | CommentConstr e -> [pp_expr e]
- | CommentString s -> [Element ("string", [], [PCData s])]
- | CommentInt i -> [PCData (string_of_int i)]
-
-let rec tmpp v loc =
- match v with
- (* Control *)
- | VernacLoad (verbose,f) ->
- xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime (loc,e) ->
- xmlApply loc (Element("time",[],[]) ::
- [tmpp e loc])
- | VernacRedirect (s, (loc,e)) ->
- xmlApply loc (Element("redirect",["path", s],[]) ::
- [tmpp e loc])
- | VernacTimeout (s,e) ->
- xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
- [tmpp e loc])
- | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
-
- (* Syntax *)
- | VernacSyntaxExtension (_, ((_, name), sml)) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- xmlReservedNotation attrs name loc
-
- | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
- | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
- | VernacDelimiters (name,Some tag) ->
- xmlScope loc "delimit" name ~attr:["delimiter",tag] []
- | VernacDelimiters (name,None) ->
- xmlScope loc "undelimit" name ~attr:[] []
- | VernacInfix (_,((_,name),sml),ce,sn) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotation (_, ce, (lstr, sml), sn) ->
- let name = snd lstr in
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacBindScope _ as x -> xmlTODO loc x
- | VernacNotationAddFormat _ as x -> xmlTODO loc x
- | VernacUniverse _
- | VernacConstraint _
- | VernacPolymorphic (_, _) as x -> xmlTODO loc x
- (* Gallina *)
- | VernacDefinition (ldk, ((_,id),_), de) ->
- let l, dk =
- match ldk with
- | Some l, dk -> (l, dk)
- | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
- let e =
- match de with
- | ProveBody (_, ce) -> ce
- | DefineBody (_, Some _, ce, None) -> ce
- | DefineBody (_, None , ce, None) -> ce
- | DefineBody (_, Some _, ce, Some _) -> ce
- | DefineBody (_, None , ce, Some _) -> ce in
- let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
- let str_id = Id.to_string id in
- (xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement) ], b) ->
- let str_tk = Kindops.string_of_theorem_kind tk in
- let str_id = Id.to_string id in
- (xmlThm str_tk str_id loc [pp_expr statement])
- | VernacStartTheoremProof _ as x -> xmlTODO loc x
- | VernacEndProof pe ->
- begin
- match pe with
- | Admitted -> xmlQed loc
- | Proved (_, Some ((_, id), Some tk)) ->
- let nam = Id.to_string id in
- let typ = Kindops.string_of_theorem_kind tk in
- xmlQed ~attr:["name", nam; "type", typ] loc
- | Proved (_, Some ((_, id), None)) ->
- let nam = Id.to_string id in
- xmlQed ~attr:["name", nam] loc
- | Proved _ -> xmlQed loc
- end
- | VernacExactProof _ as x -> xmlTODO loc x
- | VernacAssumption ((l, a), _, sbwcl) ->
- let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
- let many =
- List.length (List.flatten (List.map fst binders)) > 1 in
- let exprs =
- List.flatten (List.map pp_simple_binder binders) in
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- let kind = string_of_assumption_kind l a many in
- xmlAssumption kind loc exprs
- | VernacInductive (_, _, iednll) ->
- let kind =
- let (_, _, _, k, _),_ = List.hd iednll in
- begin
- match k with
- | Record -> "Record"
- | Structure -> "Structure"
- | Inductive_kw -> "Inductive"
- | CoInductive -> "CoInductive"
- | Class _ -> "Class"
- | Variant -> "Variant"
- end in
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (ie, dnl) -> (pp_inductive_expr ie) @
- (List.map pp_decl_notation dnl)) iednll) in
- xmlInductive kind loc exprs
- | VernacFixpoint (_, fednll) ->
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
- (List.map pp_decl_notation dnl)) fednll) in
- xmlFixpoint exprs
- | VernacCoFixpoint (_, cfednll) ->
- (* Nota: it is like VernacFixpoint without so could be merged *)
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
- (List.map pp_decl_notation dnl)) cfednll) in
- xmlCoFixpoint exprs
- | VernacScheme _ as x -> xmlTODO loc x
- | VernacCombinedScheme _ as x -> xmlTODO loc x
-
- (* Gallina extensions *)
- | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
- | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
- | VernacNameSectionHypSet _ as x -> xmlTODO loc x
- | VernacRequire (from, import, l) ->
- let import = match import with
- | None -> []
- | Some true -> ["export","true"]
- | Some false -> ["import","true"]
- in
- let from = match from with
- | None -> []
- | Some r -> ["from", Libnames.string_of_reference r]
- in
- xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (true,l) ->
- xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (false,l) ->
- xmlImport loc (List.map (fun ref ->
- xmlReference ref) l)
- | VernacCanonical r ->
- let attr =
- match r with
- | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
- | AN (Ident (_, id)) -> ["id", Id.to_string id]
- | ByNotation (_, s, _) -> ["notation", s] in
- xmlCanonicalStructure attr loc
- | VernacCoercion _ as x -> xmlTODO loc x
- | VernacIdentityCoercion _ as x -> xmlTODO loc x
-
- (* Type classes *)
- | VernacInstance _ as x -> xmlTODO loc x
-
- | VernacContext _ as x -> xmlTODO loc x
-
- | VernacDeclareInstances _ as x -> xmlTODO loc x
-
- | VernacDeclareClass _ as x -> xmlTODO loc x
-
- (* Modules and Module Types *)
- | VernacDeclareModule _ as x -> xmlTODO loc x
- | VernacDefineModule _ as x -> xmlTODO loc x
- | VernacDeclareModuleType _ as x -> xmlTODO loc x
- | VernacInclude _ as x -> xmlTODO loc x
-
- (* Solving *)
-
- | (VernacSolveExistential _) as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (recf,name,None) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacAddLoadPath (recf,name,Some dp) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
- [PCData (Names.DirPath.to_string dp)]
- | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
- | VernacAddMLPath (recf,name) ->
- xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
- | VernacChdir _ as x -> xmlTODO loc x
-
- (* State management *)
- | VernacWriteState _ as x -> xmlTODO loc x
- | VernacRestoreState _ as x -> xmlTODO loc x
-
- (* Resetting *)
- | VernacResetName _ as x -> xmlTODO loc x
- | VernacResetInitial as x -> xmlTODO loc x
- | VernacBack _ as x -> xmlTODO loc x
- | VernacBackTo _ -> PCData "VernacBackTo"
-
- (* Commands *)
- | VernacCreateHintDb _ as x -> xmlTODO loc x
- | VernacRemoveHints _ as x -> xmlTODO loc x
- | VernacHints _ as x -> xmlTODO loc x
- | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
- let name = Id.to_string name in
- let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
- xmlNotation attrs name loc [pp_expr ce]
- | VernacDeclareImplicits _ as x -> xmlTODO loc x
- | VernacArguments _ as x -> xmlTODO loc x
- | VernacArgumentsScope _ as x -> xmlTODO loc x
- | VernacReserve _ as x -> xmlTODO loc x
- | VernacGeneralizable _ as x -> xmlTODO loc x
- | VernacSetOpacity _ as x -> xmlTODO loc x
- | VernacSetStrategy _ as x -> xmlTODO loc x
- | VernacUnsetOption _ as x -> xmlTODO loc x
- | VernacSetOption _ as x -> xmlTODO loc x
- | VernacSetAppendOption _ as x -> xmlTODO loc x
- | VernacAddOption _ as x -> xmlTODO loc x
- | VernacRemoveOption _ as x -> xmlTODO loc x
- | VernacMemOption _ as x -> xmlTODO loc x
- | VernacPrintOption _ as x -> xmlTODO loc x
- | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
- | VernacGlobalCheck _ as x -> xmlTODO loc x
- | VernacDeclareReduction _ as x -> xmlTODO loc x
- | VernacPrint _ as x -> xmlTODO loc x
- | VernacSearch _ as x -> xmlTODO loc x
- | VernacLocate _ as x -> xmlTODO loc x
- | VernacRegister _ as x -> xmlTODO loc x
- | VernacComments (cl) ->
- xmlComment loc (List.flatten (List.map pp_comment cl))
-
- (* Stm backdoor *)
- | VernacStm _ as x -> xmlTODO loc x
-
- (* Proof management *)
- | VernacGoal _ as x -> xmlTODO loc x
- | VernacAbort _ as x -> xmlTODO loc x
- | VernacAbortAll -> PCData "VernacAbortAll"
- | VernacRestart as x -> xmlTODO loc x
- | VernacUndo _ as x -> xmlTODO loc x
- | VernacUndoTo _ as x -> xmlTODO loc x
- | VernacBacktrack _ as x -> xmlTODO loc x
- | VernacFocus _ as x -> xmlTODO loc x
- | VernacUnfocus as x -> xmlTODO loc x
- | VernacUnfocused as x -> xmlTODO loc x
- | VernacBullet _ as x -> xmlTODO loc x
- | VernacSubproof _ as x -> xmlTODO loc x
- | VernacEndSubproof as x -> xmlTODO loc x
- | VernacShow _ as x -> xmlTODO loc x
- | VernacCheckGuard as x -> xmlTODO loc x
- | VernacProof (tac,using) ->
- let tac = None (** FIXME *) in
- let using = Option.map (xmlSectionSubsetDescr "using") using in
- xmlProof loc (Option.List.(cons tac (cons using [])))
- | VernacProofMode name -> xmlProofMode loc name
-
- (* Toplevel control *)
- | VernacToplevelControl _ as x -> xmlTODO loc x
-
- (* For extension *)
- | VernacExtend _ as x ->
- xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Flags *)
- | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
- | VernacLocal (b,e) ->
- xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
- [tmpp e loc])
-
-let tmpp v loc =
- match tmpp v loc with
- | Element("ltac",_,_) as x -> x
- | xml -> xmlGallina loc [xml]
diff --git a/ide/texmacspp.mli b/ide/texmacspp.mli
deleted file mode 100644
index 858847fb6a..0000000000
--- a/ide/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c8ac7df5c6..935a3cab4a 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -17,6 +17,7 @@ type universes = t
type 'a check_function = universes -> 'a -> 'a -> bool
val check_leq : universe check_function
val check_eq : universe check_function
+val check_eq_level : universe_level check_function
(** The empty graph of universes *)
val empty_universes : universes
diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el
new file mode 100644
index 0000000000..4e8830f6c1
--- /dev/null
+++ b/plugins/.dir-locals.el
@@ -0,0 +1,4 @@
+((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
+ buffer-file-name ".dir-locals.el")))
+ (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq"))
+ (setq-local coq-prog-name (expand-file-name "../bin/coqtop")))))))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cc7701ad5f..18a1f02011 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -736,7 +736,7 @@ let _ =
optread = (fun () -> !keep_proof_equalities_for_injection) ;
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
-let find_positions env sigma t1 t2 =
+let find_positions env sigma ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
let s = get_sort_family_of env sigma ty1 in
@@ -767,7 +767,7 @@ let find_positions env sigma t1 t2 =
List.flatten
(List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
0 rargs1 rargs2)
- else if Sorts.List.mem InType sorts'
+ else if Sorts.List.mem InType sorts' && not no_discr
then (* see build_discriminator *)
raise (DiscrFound (List.rev posn,sp1,sp2))
else
@@ -791,13 +791,14 @@ let find_positions env sigma t1 t2 =
Inl (path,c1,c2)
let discriminable env sigma t1 t2 =
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:false t1 t2 with
| Inl _ -> true
| _ -> false
let injectable env sigma t1 t2 =
- match find_positions env sigma t1 t2 with
- | Inl _ | Inr [] | Inr [([],_,_)] -> false
+ match find_positions env sigma ~no_discr:true t1 t2 with
+ | Inl _ -> assert false
+ | Inr [] | Inr [([],_,_)] -> false
| Inr _ -> true
@@ -1032,7 +1033,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:false t1 t2 with
| Inr _ ->
tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
@@ -1414,9 +1415,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:true t1 t2 with
| Inl _ ->
- tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
+ assert false
| Inr [] ->
let suggestion =
if !keep_proof_equalities_for_injection then
@@ -1483,7 +1484,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:false t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d979c580aa..b47be3bbc0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -96,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
val rewriteInConcl : bool -> constr -> unit Proofview.tactic
+(* Tells if tactic "discriminate" is applicable *)
val discriminable : env -> evar_map -> constr -> constr -> bool
+
+(* Tells if tactic "injection" is applicable *)
val injectable : env -> evar_map -> constr -> constr -> bool
(* Subst *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 556df6e559..15cef676e6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2395,6 +2395,29 @@ let rec explicit_intro_names = function
explicit_intro_names l
| [] -> []
+let rec check_name_unicity env ok seen = function
+| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l
+| (loc, IntroNaming (IntroIdentifier id)) :: l ->
+ (try
+ ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env);
+ user_err ~loc (pr_id id ++ str" is already used.")
+ with Not_found ->
+ if List.mem_f Id.equal id seen then
+ user_err ~loc (pr_id id ++ str" is used twice.")
+ else
+ check_name_unicity env ok (id::seen) l)
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+ let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
+ List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll
+| (_, IntroAction (IntroInjection l)) :: l' ->
+ check_name_unicity env ok seen (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+ check_name_unicity env ok seen (pat::l')
+| (_, (IntroNaming (IntroAnonymous | IntroFresh _)
+ | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
+ check_name_unicity env ok seen l
+| [] -> ()
+
let wild_id = Id.of_string "_tmp"
let rec list_mem_assoc_right id = function
@@ -2530,13 +2553,21 @@ and prepare_intros_loc loc with_evars dft destopt = function
| IntroForthcoming _ -> user_err ~loc
(str "Introduction pattern for one hypothesis expected.")
+let intro_patterns_head_core with_evars b destopt bound pat =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ check_name_unicity env [] [] pat;
+ intro_patterns_core with_evars b [] [] [] destopt
+ bound 0 (fun _ l -> clear_wildcards l) pat
+ end }
+
let intro_patterns_bound_to with_evars n destopt =
- intro_patterns_core with_evars true [] [] [] destopt
- (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
+ intro_patterns_head_core with_evars true destopt
+ (Some (true,n))
let intro_patterns_to with_evars destopt =
- intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
- [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
+ intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+ destopt None
let intro_pattern_to with_evars destopt pat =
intro_patterns_to with_evars destopt [dloc,pat]
@@ -4191,6 +4222,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
let f (_,is_not_let,_,_) = is_not_let in
Array.map (fun (_,l) -> List.map f l) indsign in
let names = compute_induction_names branchletsigns names in
+ Array.iter (check_name_unicity env toclear []) names;
let tac =
(if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
(Tacticals.New.tclTHENLIST [
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 39ef05269f..afaa48463b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -408,6 +408,11 @@ modules/%.vo: modules/%.v
misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
+misc/universes.log: misc/universes/all_stdlib.v
+
+misc/universes/all_stdlib.v:
+ cd .. && $(MAKE) test-suite/$@
+
$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
@echo "TEST $<"
$(HIDE){ \
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 239edd1da3..19c9fc4423 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -2,3 +2,7 @@ Ltac f H := split; [ a H | e H ]
Ltac g := match goal with
| |- context [ if ?X then _ else _ ] => case X
end
+The command has indeed failed with message:
+H is already used.
+The command has indeed failed with message:
+H is already used.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index a7c497cfaf..9a5edb813d 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -11,3 +11,13 @@ Print Ltac f.
Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
Print Ltac g.
+
+(* Test an error message (#5390) *)
+Lemma myid (P : Prop) : P <-> P.
+Proof. split; auto. Qed.
+
+Goal True -> (True /\ True) -> True.
+Proof.
+intros H.
+Fail intros [H%myid ?].
+Fail destruct 1 as [H%myid ?].
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8f50bfb3d8..41d370ea57 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -641,6 +641,9 @@ let init_toplevel arglist =
init_library_roots ();
load_vernac_obj ();
require ();
+ (* XXX: This is incorrect in batch mode, as we will initialize
+ the STM before having done Declaremods.start_library, thus
+ state 1 is invalid. This bug was present in 8.5/8.6. *)
Stm.init ();
let sid = load_rcfile (Stm.get_current_state ()) in
(* XXX: We ignore this for now, but should be threaded to the toplevels *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index eaf685b184..deb2cc1e3f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -126,6 +126,16 @@ let rec interp_vernac sid (loc,com) =
let f = Loadpath.locate_file fname in
load_vernac verbosely sid f
| v ->
+
+ (* XXX: We need to run this before add as the classification is
+ highly dynamic and depends on the structure of the
+ document. Hopefully this is fixed when VtBack can be removed
+ and Undo etc... are just interpreted regularly. *)
+ let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
+ | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+ | _ -> false
+ in
+
let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
(* Main STM interaction *)
@@ -139,11 +149,12 @@ let rec interp_vernac sid (loc,com) =
if check_proof then Stm.finish ();
(* We could use a more refined criteria that depends on the
- vernac. For now we imitate the old approach. *)
- let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
- not (Proof_global.there_are_pending_proofs ()) in
+ vernac. For now we imitate the old approach and rely on the
+ classification. *)
+ let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+ is_proof_step && Proof_global.there_are_pending_proofs () in
- if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+ if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
nsid
in
try
@@ -153,7 +164,9 @@ let rec interp_vernac sid (loc,com) =
let com = if !Flags.time then VernacTime (loc,com) else com in
interp com
with reraise ->
- ignore(Stm.edit_at sid);
+ (* XXX: In non-interactive mode edit_at seems to do very weird
+ things, so we better avoid it while we investigate *)
+ if not !Flags.batch_mode then ignore(Stm.edit_at sid);
let (reraise, info) = CErrors.push reraise in
let loc' = Option.default Loc.ghost (Loc.get_loc info) in
if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5233fab151..24cb9c886e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -631,6 +631,16 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+let it_mkLambda_or_LetIn_or_clean t ctx =
+ let open Context.Rel.Declaration in
+ let fold t decl =
+ if is_local_assum decl then mkLambda_or_LetIn decl t
+ else
+ if noccurn 1 t then subst1 mkProp t
+ else mkLambda_or_LetIn decl t
+ in
+ Context.Rel.fold_inside fold ctx ~init:t
+
let declare_obligation prg obl body ty uctx =
let body = prg.prg_reduce body in
let ty = Option.map prg.prg_reduce ty in
@@ -664,7 +674,7 @@ let declare_obligation prg obl body ty uctx =
if poly then
Some (DefinedObl constant)
else
- Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
+ Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
notations obls impls kind reduce hook =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:14:47 +0000