diff options
| author | filliatr | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 /kernel/safe_typing.ml | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
syntaxe AST Inversion + commentaires ocamlweb autour de $
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 642673a8a3..c0e700a130 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -312,6 +312,7 @@ let add_discharged_constant sp r env = | None -> add_parameter sp typ env | Some c -> + (* let c = hcons1_constr c in *) let (jtyp,cst) = safe_infer env typ in let env' = add_constraints cst env in let ids = @@ -319,7 +320,7 @@ let add_discharged_constant sp r env = (global_vars_set (body_of_type jtyp.uj_val)) in let cb = { const_kind = kind_of_path sp; - const_body = body; + const_body = Some c; const_type = assumption_of_judgment env' Evd.empty jtyp; const_hyps = keep_hyps ids (named_context env); const_constraints = cst; |