diff options
Diffstat (limited to 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index c6a1df1d9..429e93aa4 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -66,22 +66,12 @@ let is_tactic_proof pf = (pf.subproof <> None) (* Constraints for existential variables *) (*******************************************************************) -(* A local constraint is just a set of section_paths *) - -(* recall : type local_constraints = Intset.t *) - -(* A global constraint is a mappings of existential variables - with some extra information for the program and mimick - tactics. *) - -type global_constraints = enamed_declarations timestamped - (* A readable constraint is a global constraint plus a focus set of existential variables and a signature. *) type evar_recordty = { hyps : named_context; - decls : enamed_declarations } + decls : evar_map } and readable_constraints = evar_recordty timestamped |