diff options
| author | herbelin | 2001-09-09 15:11:26 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-09 15:11:26 +0000 |
| commit | 2ec6a91a4270d2941cee84f67599a3d28285833f (patch) | |
| tree | bf67fc996db1a7786c98fd19d247bc397ff8265c /pretyping/cases.ml | |
| parent | 60d3ce883c895c75b6b952e60a3600b0af7bfbee (diff) | |
Préparation du prétypage à la mise en place d'univers algébriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1936 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 038f70c2c2..864632ebb0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -60,7 +60,7 @@ let error_needs_inversion k env x t = (* A) Typing old cases *) (* This was previously in Indrec but creates existential holes *) -let mkExistential isevars env = new_isevar isevars env dummy_sort CCI +let mkExistential isevars env = new_isevar isevars env (new_Type ()) CCI let norec_branch_scheme env isevars cstr = let rec crec env = function @@ -958,9 +958,9 @@ let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) = | None -> infer_predicate env isevars typs cstrs indf in let typ = whd_beta (applist (pred, realargs)) in if dep then - (pred, whd_beta (applist (typ, [current])), Type Univ.dummy_univ) + (pred, whd_beta (applist (typ, [current])), new_Type ()) else - (pred, typ, Type Univ.dummy_univ) + (pred, typ, new_Type ()) (************************************************************************) (* Sorting equation by constructor *) @@ -1328,7 +1328,7 @@ let build_expected_arity env isevars isdep tomatchl = | _,NotInd _ -> None in let rec buildrec n env = function - | [] -> dummy_sort + | [] -> new_Type () | tm::ltm -> match cook n tm with | None -> buildrec n env ltm |