diff options
| author | letouzey | 2012-05-29 11:08:50 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:50 +0000 |
| commit | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (patch) | |
| tree | 44b4f39e7f92f29f4626d4aa8265fe68eb129111 /plugins/funind/glob_term_to_relation.ml | |
| parent | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (diff) | |
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ccf2caaf56..95c6a6d997 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1256,13 +1256,13 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b let rec rebuild_return_type rt = match rt with - | Topconstr.CProdN(loc,n,t') -> - Topconstr.CProdN(loc,n,rebuild_return_type t') - | Topconstr.CLetIn(loc,na,t,t') -> - Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], - Topconstr.Default Decl_kinds.Explicit,rt], - Topconstr.CSort(dummy_loc,GType None)) + | Constrexpr.CProdN(loc,n,t') -> + Constrexpr.CProdN(loc,n,rebuild_return_type t') + | Constrexpr.CLetIn(loc,na,t,t') -> + Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') + | _ -> Constrexpr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], + Constrexpr.Default Decl_kinds.Explicit,rt], + Constrexpr.CSort(dummy_loc,GType None)) let do_build_inductive @@ -1302,10 +1302,10 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else - Topconstr.CProdN + Constrexpr.CProdN (dummy_loc, [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc @@ -1368,10 +1368,10 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, acc) else - Topconstr.CProdN + Constrexpr.CProdN (dummy_loc, [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc @@ -1390,9 +1390,9 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) + Constrexpr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) else - Topconstr.LocalRawAssum + Constrexpr.LocalRawAssum ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) ) rels_params |