diff options
| -rw-r--r-- | contrib/subtac/Utils.v | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 3 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 15 | ||||
| -rw-r--r-- | ide/highlight.mll | 9 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
5 files changed, 22 insertions, 11 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 4ef4f3ece..102fa94ad 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -12,8 +12,8 @@ Notation "( x & ? )" := (@exist _ _ x _) : core_scope. Notation " ! " := (False_rect _ _). -(* Logical if : keep a trace of the control flow in obligations. *) -Notation " 'lif' b 'then' e 'else' f " := (match b with true => e | false => f end) (at level 30). +Require Import Coq.Bool.Sumbool. +Notation "'dec'" := (sumbool_of_bool) (at level 0). Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. intros. diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 6086bd547..17110c058 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -2094,11 +2094,10 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let _, j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - let ty = tycon_constr in let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = ty; } + uj_type = out_some (valcon_of_tycon tycon0); } in j (* inh_conv_coerce_to_tycon loc env isevars j tycon0 *) else diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 4dde60111..a8edc4061 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -77,10 +77,17 @@ let commands = [ ["Module"; "Module Type"; "Mutual Inductive";]; - ["Notation";]; - ["Opaque";]; + ["Notation"; + "Next Obligation";]; + ["Opaque"; + "Obligations Tactic";]; ["Parameter"; - "Proof."]; + "Proof."; + "Program Definition"; + "Program Fixpoint"; + "Program Lemma"; + "Program Theorem"; + ]; ["Qed."; ]; ["Read Module"; @@ -155,6 +162,8 @@ let state_preserving = [ "Extraction Module"; "Inspect"; "Locate"; + + "Obligations"; "Print"; "Print All."; "Print Classes"; diff --git a/ide/highlight.mll b/ide/highlight.mll index ea2f5bca4..c033a6af5 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -28,7 +28,8 @@ "Notation"; "Proof" ; "Print"; "Qed" ; "Require" ; "Reset"; "Undo"; "Save" ; "Section" ; "Unset" ; - "Set" ; "Notation" + "Set" ; "Notation"; + "Implicit"; "Arguments"; "Unfold"; "Resolve" ]; Hashtbl.mem h @@ -36,7 +37,7 @@ let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; - "end"; "as"; "let"; "if"; "then"; "else"; "return"; + "end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return"; "Prop"; "Set"; "Type"]; Hashtbl.mem h @@ -45,7 +46,7 @@ List.iter (fun s -> Hashtbl.add h s ()) [ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ; "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ; - "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; + "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters" ]; @@ -74,12 +75,14 @@ let declaration = "Inductive" | "CoInductive" | "Record" | "Structure" | "Fixpoint" | "CoFixpoint" + rule next_order = parse | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } | "Module Type" { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } + | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" } | ident as id { if is_keyword id then lexeme_start lexbuf, lexeme_end lexbuf, "kwd" diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 4bd897321..45017db8d 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -51,7 +51,7 @@ let is_keyword = "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant"; "while"; i*) (*i (* coq terms *) *) - "match"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":=" + "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":=" ] (*s Current Coq module *) |