From 8ad5f5726283c69a71f7ee0f2d12ce94b707b5a6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 17:39:03 +0200
Subject: Bug 4284: Tentative bugfix for detyping exception.

---
 ide/ide_slave.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dc52ea9aad..6618dc7ef9 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -185,12 +185,14 @@ let process_goal sigma g =
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
     string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
-  let process_hyp d =
+  let process_hyp d (env,l) =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
-    (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in
-  let hyps =
-    List.map process_hyp
-      (Termops.compact_named_context_reverse (Environ.named_context env)) in
+    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+      (List.fold_right Environ.push_named d' env,
+       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+  let (_env, hyps) =
+    Context.fold_named_list_context process_hyp
+      (Termops.compact_named_context_reverse (Environ.named_context env)) ~init:(min_env,[]) in
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let export_pre_goals pgs =
-- 
cgit v1.2.3


From a198b3f7402d4b275a7fc67ece827843f00dadf0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 17:57:54 +0200
Subject: Ide: fix bug #4284 for good

Correct folding order over the named_list_context.
---
 ide/ide_slave.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 6618dc7ef9..94f9c9a361 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -192,8 +192,8 @@ let process_goal sigma g =
        (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
   let (_env, hyps) =
     Context.fold_named_list_context process_hyp
-      (Termops.compact_named_context_reverse (Environ.named_context env)) ~init:(min_env,[]) in
-  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
+      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
+  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let export_pre_goals pgs =
   {
-- 
cgit v1.2.3


From 591e7e484d544e958595a0fb784336ae050a9c74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:13:47 +0200
Subject: Highlighting Universe in CoqIDE.

---
 ide/coq.lang | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coq.lang b/ide/coq.lang
index c65432bdb7..89f93a705e 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -29,7 +29,7 @@
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
     <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
-    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex>
     <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
     <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
     <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
-- 
cgit v1.2.3


From 7351bf1c179c4feebf4d93437625ea358dc59420 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 11 Jul 2015 23:49:31 +0200
Subject: CoqIDE: recenter on backtrack (Close: #4277)

---
 ide/coqOps.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2387d65c30..c6d3149475 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -669,7 +669,10 @@ object(self)
       push_info "Coq is undoing" in
     let conclusion () =
       pop_info ();
-      if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+      if move_insert then begin
+        buffer#place_cursor ~where:self#get_start_of_input;
+        script#recenter_insert;
+      end;
       let start = self#get_start_of_input in
       let stop = self#get_end_of_input in
       Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
-- 
cgit v1.2.3