diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7fa60737d..19065bebb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -126,11 +126,11 @@ let pretype_ref loc isevars env = function pretype vtcon isevars env (abst_value cstr) else error "Cannot typecheck an unevaluable abstraction" *) - -| REVar (sp,ids) -> +| REVar (sp,ids) -> error " Not able to type terms with dependent subgoals" +(* Not able to type goal existential yet let cstr = mkConst sp (ctxt_of_ids ids) in make_judge cstr (type_of_existential env !isevars cstr) - +*) | RInd ((sp,i),ids) -> let cstr = mkMutInd sp i (ctxt_of_ids ids) in make_judge cstr (type_of_inductive env !isevars cstr) |