Implemented a full-fledged equality on [constr_expr]. By the way,

some cleaning of the interface and moving of code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 224 insertions, 141 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index b9469bdf3..d49219114 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -12,6 +12,7 @@ open Names
 open Libnames
 open Glob_term
 open Constrexpr
+open Misctypes
 open Decl_kinds
 
 (***********************)
@@ -22,6 +23,11 @@ let binding_kind_eq bk1 bk2 = match bk1, bk2 with
 | Implicit, Implicit -> true
 | _ -> false
 
+let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
+| AbsLambda, AbsLambda -> true
+| AbsPi, AbsPi -> true
+| _ -> false
+
 let binder_kind_eq b1 b2 = match b1, b2 with
 | Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
@@ -40,6 +46,181 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
+let prim_token_eq t1 t2 = match t1, t2 with
+| Numeral i1, Numeral i2 -> Bigint.equal i1 i2
+| String s1, String s2 -> String.equal s1 s2
+| _ -> false
+
+let explicitation_eq ex1 ex2 = match ex1, ex2 with
+| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
+  Int.equal i1 i2 && Option.equal id_eq id1 id2
+| ExplByName id1, ExplByName id2 ->
+  id_eq id1 id2
+| _ -> false
+
+let eq_located f (_, x) (_, y) = f x y
+
+let rec cases_pattern_expr_eq p1 p2 =
+  if p1 == p2 then true
+  else match p1, p2 with
+  | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) ->
+      id_eq i1 i2 && cases_pattern_expr_eq a1 a2
+  | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
+      eq_reference c1 c2 &&
+      List.equal cases_pattern_expr_eq a1 a2 &&
+      List.equal cases_pattern_expr_eq b1 b2
+  | CPatAtom(_,r1), CPatAtom(_,r2) ->
+      Option.equal eq_reference r1 r2
+  | CPatOr (_, a1), CPatOr (_, a2) ->
+      List.equal cases_pattern_expr_eq a1 a2
+  | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) ->
+    String.equal n1 n2 &&
+    cases_pattern_notation_substitution_eq s1 s2 &&
+    List.equal cases_pattern_expr_eq l1 l2
+  | CPatPrim(_,i1), CPatPrim(_,i2) ->
+      prim_token_eq i1 i2
+  | CPatRecord (_, l1), CPatRecord (_, l2) ->
+      let equal (r1, e1) (r2, e2) =
+        eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
+      in
+      List.equal equal l1 l2
+  | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) ->
+      String.equal s1 s2 && cases_pattern_expr_eq e1 e2
+  | _ -> false
+
+and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) =
+  List.equal cases_pattern_expr_eq s1 s2 &&
+  List.equal (List.equal cases_pattern_expr_eq) n1 n2
+
+let rec constr_expr_eq e1 e2 =
+  if e1 == e2 then true
+  else match e1, e2 with
+  | CRef r1, CRef r2 -> eq_reference r1 r2
+  | CFix(_,id1,fl1), CFix(_,id2,fl2) ->
+      eq_located id_eq id1 id2 &&
+      List.equal fix_expr_eq fl1 fl2
+  | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) ->
+      eq_located id_eq id1 id2 &&
+      List.equal cofix_expr_eq fl1 fl2
+  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
+      List.equal binder_expr_eq bl1 bl2 &&
+      constr_expr_eq a1 a2
+  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
+      List.equal binder_expr_eq bl1 bl2 &&
+      constr_expr_eq a1 a2
+  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) ->
+      name_eq na1 na2 &&
+      constr_expr_eq a1 a2 &&
+      constr_expr_eq b1 b2
+  | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) ->
+      Option.equal Int.equal proj1 proj2 &&
+      eq_reference r1 r2 &&
+      List.equal constr_expr_eq al1 al2
+  | CApp(_,(proj1,e1),al1), CApp(_,(proj2,e2),al2) ->
+      Option.equal Int.equal proj1 proj2 &&
+      constr_expr_eq e1 e2 &&
+      List.equal args_eq al1 al2
+  | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+    let field_eq (r1, e1) (r2, e2) =
+      eq_reference r1 r2 && constr_expr_eq e1 e2
+    in
+    Option.equal constr_expr_eq e1 e2 &&
+    List.equal field_eq l1 l2
+  | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
+      (** Don't care about the case_style *)
+      Option.equal constr_expr_eq r1 r2 &&
+      List.equal case_expr_eq a1 a2 &&
+      List.equal branch_expr_eq brl1 brl2
+  | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) ->
+    List.equal (eq_located name_eq) n1 n2 &&
+    Option.equal (eq_located name_eq) m1 m2 &&
+    Option.equal constr_expr_eq e1 e2 &&
+    constr_expr_eq t1 t2 &&
+    constr_expr_eq b1 b2
+  | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) ->
+    constr_expr_eq e1 e2 &&
+    Option.equal (eq_located name_eq) n1 n2 &&
+    Option.equal constr_expr_eq r1 r2 &&
+    constr_expr_eq t1 t2 &&
+    constr_expr_eq f1 f2
+  | CHole _, CHole _ -> true
+  | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) ->
+    (b1 : bool) == b2 && id_eq i1 i2
+  | CEvar (_, ev1, c1), CEvar (_, ev2, c2) ->
+    Int.equal ev1 ev2 &&
+    Option.equal (List.equal constr_expr_eq) c1 c2
+  | CSort(_,s1), CSort(_,s2) ->
+    Glob_ops.glob_sort_eq s1 s2
+  | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
+      constr_expr_eq a1 a2 &&
+      constr_expr_eq b1 b2
+  | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
+      constr_expr_eq a1 a2
+  | CNotation(_, n1, s1), CNotation(_, n2, s2) ->
+      String.equal n1 n2 &&
+      constr_notation_substitution_eq s1 s2
+  | CPrim(_,i1), CPrim(_,i2) ->
+    prim_token_eq i1 i2
+  | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) ->
+    binding_kind_eq bk1 bk2 &&
+    Option.equal abstraction_kind_eq ak1 ak2 &&
+    constr_expr_eq e1 e2
+  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) ->
+    String.equal s1 s2 &&
+    constr_expr_eq e1 e2
+  | _ -> false
+
+and args_eq (a1,e1) (a2,e2) =
+  Option.equal (eq_located explicitation_eq) e1 e2 &&
+  constr_expr_eq a1 a2
+
+and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+  constr_expr_eq e1 e2 &&
+  Option.equal (eq_located name_eq) n1 n2 &&
+  Option.equal cases_pattern_expr_eq p1 p2
+
+and branch_expr_eq (_, p1, e1) (_, p2, e2) =
+  List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 &&
+  constr_expr_eq e1 e2
+
+and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
+  (** Don't care about the [binder_kind] *)
+  List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2
+
+and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
+  (eq_located id_eq id1 id2) &&
+  Option.equal (eq_located id_eq) j1 j2 &&
+  recursion_order_expr_eq r1 r2 &&
+  List.equal local_binder_eq bl1 bl2 &&
+  constr_expr_eq a1 a2 &&
+  constr_expr_eq b1 b2
+
+and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
+  (eq_located id_eq id1 id2) &&
+  List.equal local_binder_eq bl1 bl2 &&
+  constr_expr_eq a1 a2 &&
+  constr_expr_eq b1 b2
+
+and recursion_order_expr_eq r1 r2 = match r1, r2 with
+| CStructRec, CStructRec -> true
+| CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2
+| CMeasureRec (e1, o1), CMeasureRec (e2, o2) ->
+  constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
+| _ -> false
+
+and local_binder_eq l1 l2 = match l1, l2 with
+| LocalRawDef (n1, e1), LocalRawDef (n2, e2) ->
+  eq_located name_eq n1 n2 && constr_expr_eq e1 e2
+| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) ->
+  (** Don't care about the [binder_kind] *)
+  List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2
+| _ -> false
+
+and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
+  List.equal constr_expr_eq e1 e2 &&
+  List.equal (List.equal constr_expr_eq) el1 el2 &&
+  List.equal (List.equal local_binder_eq) bl1 bl2
+
 let constr_loc = function
   | CRef (Ident (loc,_)) -> loc
   | CRef (Qualid (loc,_)) -> loc
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index bd118bbce..8eb88f70d 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -17,18 +17,32 @@ open Constrexpr
 
 (** Constrexpr_ops: utilities on [constr_expr] *)
 
-val constr_loc : constr_expr -> Loc.t
+(** {6 Equalities on [constr_expr] related types} *)
 
-val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
+val explicitation_eq : explicitation -> explicitation -> bool
+(** Equality on [explicitation]. *)
 
-val local_binders_loc : local_binder list -> Loc.t
+val constr_expr_eq : constr_expr -> constr_expr -> bool
+(** Equality on [constr_expr]. This is a syntactical one, which is oblivious to
+    some parsing details, including locations. *)
+
+val local_binder_eq : local_binder -> local_binder -> bool
+(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
 
 val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
+(** Equality on [binding_kind] *)
 
 val binder_kind_eq : binder_kind -> binder_kind -> bool
+(** Equality on [binder_kind] *)
 
-val default_binder_kind : binder_kind
+(** {6 Retrieving locations} *)
+
+val constr_loc : constr_expr -> Loc.t
+val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
+val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
+val local_binders_loc : local_binder list -> Loc.t
+
+(** {6 Constructors}*)
 
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
@@ -38,24 +52,36 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
-val coerce_reference_to_id : reference -> identifier
-val coerce_to_id : constr_expr -> identifier located
-val coerce_to_name : constr_expr -> name located
-
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
-(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
 val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+(** Same as [abstract_constr_expr], with location *)
+
 val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+(** Same as [prod_constr_expr], with location *)
 
-(** For binders parsing *)
+(** {6 Destructors}*)
 
-(** With let binders *)
-val names_of_local_assums : local_binder list -> name located list
+val coerce_reference_to_id : reference -> identifier
+(** FIXME: nothing to do here *)
+
+val coerce_to_id : constr_expr -> identifier located
+(** Destruct terms of the form [CRef (Ident _)]. *)
+
+val coerce_to_name : constr_expr -> name located
+(** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
+
+(** {6 Binder manipulation} *)
+
+val default_binder_kind : binder_kind
 
-(** Does not take let binders into account *)
 val names_of_local_binders : local_binder list -> name located list
+(** Retrieve a list of binding names from a list of binders. *)
+
+val names_of_local_assums : local_binder list -> name located list
+(** Same as [names_of_local_binders], but does not take the [let] bindings into
+    account. *)
 
 val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit)
   -> Glob_term.glob_constr -> raw_cases_pattern_expr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 72577d866..d0be33031 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -155,116 +155,6 @@ let extern_reference loc vars r =
   else
     Qualid (loc,shortest_qualid_of_global vars r)
 
-
-(************************************************************************)
-(* Equality up to location (useful for translator v8) *)
-
-let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral i1, Numeral i2 -> Bigint.equal i1 i2
-| String s1, String s2 -> String.equal s1 s2
-| _ -> false
-
-(** ppedrot: FIXME, EVERYTHING IS WRONG HERE! *)
-
-let rec check_same_pattern p1 p2 =
-  match p1, p2 with
-    | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when id_eq i1 i2 ->
-        check_same_pattern a1 a2
-    | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) when eq_reference c1 c2 ->
-        let () = List.iter2 check_same_pattern a1 a2 in
-        List.iter2 check_same_pattern b1 b2
-    | CPatAtom(_,r1), CPatAtom(_,r2) when Option.equal eq_reference r1 r2 -> ()
-    | CPatPrim(_,i1), CPatPrim(_,i2) when prim_token_eq i1 i2 -> ()
-    | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when String.equal s1 s2 ->
-        check_same_pattern e1 e2
-    | _ -> failwith "not same pattern"
-
-let check_same_ref r1 r2 =
-  if not (eq_reference r1 r2) then failwith "not same ref"
-
-let eq_located f (_, x) (_, y) = f x y
-
-let same_id (id1, c1) (id2, c2) =
-  Option.equal (eq_located id_eq) id1 id2 && Pervasives.(=) c1 c2
-
-let rec check_same_type ty1 ty2 =
-  match ty1, ty2 with
-  | CRef r1, CRef r2 -> check_same_ref r1 r2
-  | CFix(_,id1,fl1), CFix(_,id2,fl2) when eq_located id_eq id1 id2 ->
-      List.iter2 (fun ((_, id1),i1,bl1,a1,b1) ((_, id2),i2,bl2,a2,b2) ->
-        if not (id_eq id1 id2) || not (same_id i1 i2) then failwith "not same fix";
-        check_same_fix_binder bl1 bl2;
-        check_same_type a1 a2;
-        check_same_type b1 b2)
-        fl1 fl2
-  | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) when eq_located id_eq id1 id2 ->
-      List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
-        if not (eq_located id_eq id1 id2) then failwith "not same fix";
-        check_same_fix_binder bl1 bl2;
-        check_same_type a1 a2;
-        check_same_type b1 b2)
-        fl1 fl2
-  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
-      List.iter2 check_same_binder bl1 bl2;
-      check_same_type a1 a2
-  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
-      List.iter2 check_same_binder bl1 bl2;
-      check_same_type a1 a2
-  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when name_eq na1 na2 ->
-      check_same_type a1 a2;
-      check_same_type b1 b2
-  | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when Option.equal Int.equal proj1 proj2 ->
-      check_same_ref r1 r2;
-      List.iter2 check_same_type al1 al2
-  | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
-      check_same_type e1 e2;
-      let check_args (a1,e1) (a2,e2) =
-        let eq_expl = eq_located Constrintern.explicitation_eq in
-        if not (Option.equal eq_expl e1 e2) then failwith "not same expl";
-        check_same_type a1 a2
-      in
-      List.iter2 check_args al1 al2
-  | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
-      List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
-      List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
-        List.iter2 (Loc.located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
-        check_same_type r1 r2) brl1 brl2
-  | CHole _, CHole _ -> ()
-  | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) when (b1 : bool) == b2 && id_eq i1 i2 -> ()
-  | CSort(_,s1), CSort(_,s2) when glob_sort_eq s1 s2 -> ()
-  | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
-      check_same_type a1 a2;
-      check_same_type b1 b2
-  | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
-      check_same_type a1 a2
-  | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when String.equal n1 n2 ->
-      List.iter2 check_same_type e1 e2;
-      List.iter2 (List.iter2 check_same_type) el1 el2;
-      List.iter2 check_same_fix_binder bl1 bl2
-  | CPrim(_,i1), CPrim(_,i2) when prim_token_eq i1 i2 -> ()
-  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when String.equal s1 s2 ->
-      check_same_type e1 e2
-  | _ when Pervasives.(=) ty1 ty2 -> () (** FIXME *)
-  | _ -> failwith "not same type"
-
-and check_same_binder (nal1,_,e1) (nal2,_,e2) =
-  List.iter2 (fun (_,na1) (_,na2) ->
-    if not (name_eq na1 na2) then failwith "not same name") nal1 nal2;
-  check_same_type e1 e2
-
-and check_same_fix_binder bl1 bl2 =
-  List.iter2 (fun b1 b2 ->
-    match b1,b2 with
-        LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) ->
-          check_same_binder (nal1,k,ty1) (nal2,k',ty2)
-      | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
-          check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
-      | _ -> failwith "not same binder") bl1 bl2
-
-let is_same_type c d =
-  try let () = check_same_type c d in true
-  with Failure _ | Invalid_argument _ -> false
-
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
@@ -865,7 +755,7 @@ and factorize_prod scopes vars na bk aty c =
   let c = extern_typ scopes vars c in
   match na, c with
   | Name id, CProdN (loc,[nal,Default bk',ty],c)
-      when binding_kind_eq bk bk' && is_same_type aty ty
+      when binding_kind_eq bk bk' && constr_expr_eq aty ty
       & not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
@@ -875,7 +765,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
   let c = sub_extern inctx scopes vars c in
   match c with
   | CLambdaN (loc,[nal,Default bk',ty],c)
-      when binding_kind_eq bk bk' && is_same_type aty ty
+      when binding_kind_eq bk bk' && constr_expr_eq aty ty
       & not (occur_name na ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
@@ -893,7 +783,7 @@ and extern_local_binder scopes vars = function
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
       (match extern_local_binder scopes (name_fold Idset.add na vars) l with
           (assums,ids,LocalRawAssum(nal,k,ty')::l)
-            when is_same_type ty ty' &
+            when constr_expr_eq ty ty' &
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 91ad86381..0ca25656f 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -22,8 +22,6 @@ open Notation_term
 open Notation
 open Misctypes
 
-val is_same_type : constr_expr -> constr_expr -> bool
-
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f1316bbfa..e4df61c47 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1188,13 +1188,6 @@ let intern_ind_pattern genv env pat =
 (**********************************************************************)
 (* Utilities for application                                          *)
 
-let explicitation_eq ex1 ex2 = match ex1, ex2 with
-| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
-  Int.equal i1 i2 && Option.equal id_eq id1 id2
-| ExplByName id1, ExplByName id2 ->
-  id_eq id1 id2
-| _ -> false
-
 let merge_impargs l args =
   let test x = function
   | (_, Some (_, y)) -> explicitation_eq x y
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6e2c9e883..28e7e2985 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -188,8 +188,3 @@ val parsing_explicit : bool ref
 
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
-
-(** Nothing to do here *)
-
-val explicitation_eq : explicitation -> explicitation -> bool
-