diff options
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 5410e724a..a811b29b8 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -853,17 +853,6 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift lident , bindlist , Some cstr_expr , lcstor_expr - -let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = - match rdecl with - | (nme,None,t) -> - let traw = Detyping.detype false [] [] t in - GProd (Loc.ghost,nme,Explicit,traw,t2) - | (_,Some _,_) -> assert false - - - - let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> |