diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-13 20:13:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-13 20:13:10 +0200 |
| commit | cbb41129f15623ba5be50026f930e0435c9f5259 (patch) | |
| tree | a865d2dbdeb2bf628a863af8183741b6a55cc8bc /toplevel | |
| parent | 36f95a197b106b928a3fc99d7ee5904099a654e4 (diff) | |
| parent | bb43103f7ecea16e634d448215f24d6d55d56eb1 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 10 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
2 files changed, 7 insertions, 5 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ad848ccfc..e17cd2086 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -69,12 +69,12 @@ 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 + | 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) (** Ad-hoc reductions *) @@ -323,6 +323,8 @@ let 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 () diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 52117f13f..b22d53f54 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -827,7 +827,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else 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) = |