diff options
| author | jforest | 2006-06-23 16:12:45 +0000 |
|---|---|---|
| committer | jforest | 2006-06-23 16:12:45 +0000 |
| commit | 3dfe56ca4de86e1e4e7779a4ac0534f36909644e (patch) | |
| tree | 8bfeabcb8ea582d40612cbd71bfbd1defed2e722 /contrib | |
| parent | b296023d46415b19a055a24750006e7ff51f29b3 (diff) | |
Passage des graphes de Function dans Type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index b6f26dfdd3..66ee42bb46 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -900,13 +900,6 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) in List.rev !l -(* (Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,Anonymous)],returned_types.(i)], - Topconstr.CSort(dummy_loc, RProp Null ) - ) - ) -*) let rec rebuild_return_type rt = match rt with | Topconstr.CProdN(loc,n,t') -> @@ -915,7 +908,7 @@ let rec rebuild_return_type rt = Topconstr.CArrow(loc,t,rebuild_return_type t') | Topconstr.CLetIn(loc,na,t,t') -> Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc, RProp Null)) + | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None)) let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) returned_types (rtl:rawconstr list) = @@ -938,13 +931,6 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo (* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *) fst ( rebuild_cons nb_args relnames.(i) -(* (List.map *) -(* (function *) -(* (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__") *) -(* | Name id, _,_ -> mkRVar id *) -(* ) *) -(* funsargs.(i) *) -(* ) *) [] [] rt |