diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-09 15:01:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-09 15:01:54 +0000 |
| commit | 1e4c9c6dd74162c5fd75de59f1cab117e458e8de (patch) | |
| tree | 77dc73065ba7879147af5372482a745f7ce07cae /toplevel | |
| parent | 984e59594c751b842a26d251ed312819e6e9641c (diff) | |
Mécanisme pour faire remonter les contraintes de typage sur les variables de section au niveau du discharge, sans avoir à garder tout l'environnement de la section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index c8e031bb8..a9c1273e8 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -171,6 +171,7 @@ type discharge_operation = | Objdef of constant_path | Coercion of coercion_entry | Require of module_reference + | Constraints of Univ.constraints (* Main function to traverse the library segment and compute the various discharge operations. *) @@ -180,13 +181,13 @@ let process_object oldenv dir sec_sp let tag = object_tag lobj in match tag with | "VARIABLE" -> - let ((id,c,t),stre,sticky) = get_variable sp in + let ((id,c,t),cst,stre,sticky) = get_variable_with_constraints sp in (* VARIABLE means local (entry Variable/Hypothesis/Local and are *) (* always discharged *) (* if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then *) - (ops,id::ids_to_discard,work_alist) + (Constraints cst :: ops, id :: ids_to_discard, work_alist) (* else let imp = is_implicit_var sp in @@ -302,6 +303,7 @@ let process_operation = function begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end | Coercion y -> add_new_coercion y | Require y -> reload_module y + | Constraints y -> Global.add_constraints y let catch_not_found f x = try f x |