From 78102fedf6b1dca94cf2695bb1ba2000d4f76db9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jun 2016 15:08:16 +0200
Subject: Fixing bug in printing CannotSolveConstraint (collision of context
 names).

---
 toplevel/himsg.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3ff2d3fb18..fa47cc4311 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -67,10 +67,10 @@ let rec contract3' env a b c = function
   | NotSameArgSize | NotSameHead | NoCanonicalStructure
   | MetaOccurInBody _ | InstanceNotSameType _
   | UnifUnivInconsistency _ as x -> contract3 env a b c, x
-  | CannotSolveConstraint ((pb,env,t,u),x) ->
-      let env,t,u = contract2 env t u in
+  | CannotSolveConstraint ((pb,env',t,u),x) ->
+      let env',t,u = contract2 env' t u in
       let y,x = contract3' env a b c x in
-      y,CannotSolveConstraint ((pb,env,t,u),x)
+      y,CannotSolveConstraint ((pb,env',t,u),x)
 
 (** Printers *)
 
-- 
cgit v1.2.3


From 1f772656fa4bb6899ffea84ad5483e9690bbdc08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jun 2016 16:00:23 +0200
Subject: Reserve exception "ConversionFailed" in unification for failure of
 conversion on closed terms.

This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
---
 toplevel/himsg.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index fa47cc4311..244174f651 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -65,7 +65,7 @@ let rec contract3' env a b c = function
       let (env',t1,t2) = contract2 env' t1 t2 in
       contract3 env a b c, ConversionFailed (env',t1,t2)
   | NotSameArgSize | NotSameHead | NoCanonicalStructure
-  | MetaOccurInBody _ | InstanceNotSameType _
+  | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
   | UnifUnivInconsistency _ as x -> contract3 env a b c, x
   | CannotSolveConstraint ((pb,env',t,u),x) ->
       let env',t,u = contract2 env' t u in
@@ -310,6 +310,8 @@ let rec explain_unification_error env sigma p1 p2 = function
         (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++
         str " == " ++ pr_lconstr_env env sigma u)
         :: aux t u e
+     | ProblemBeyondCapabilities ->
+        []
      in
      match aux p1 p2 e with
      | [] -> mt ()
-- 
cgit v1.2.3


From 87be9070b3415f31027b78165b213de34c168043 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Jun 2016 11:27:22 +0200
Subject: Tentatively fixing misguiding error message with "binder" type in
 non-recursive notations (#4815).

---
 toplevel/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2ccd27acb9..92208e3046 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -982,7 +982,7 @@ let make_interpretation_type isrec = function
   | NtnInternTypeConstr when isrec -> NtnTypeConstrList
   | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
   | NtnInternTypeBinder when isrec -> NtnTypeBinderList
-  | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
+   | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders."
 
 let make_interpretation_vars recvars allvars =
   let eq_subscope (sc1, l1) (sc2, l2) =
-- 
cgit v1.2.3